fin2i2

Description: A II-finite set contains minimal elements for every nonempty chain. (Contributed by Mario Carneiro, 16-May-2015)

		Ref	Expression
	Assertion	fin2i2	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → ∩ 𝐵 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		simplr	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → 𝐵 ⊆ 𝒫 𝐴 )
2		simpll	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → 𝐴 ∈ Fin^II )
3		ssrab2	⊢ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ⊆ 𝒫 𝐴
4	3	a1i	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ⊆ 𝒫 𝐴 )
5		simprl	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → 𝐵 ≠ ∅ )
6		fin23lem7	⊢ ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ∧ 𝐵 ≠ ∅ ) → { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ≠ ∅ )
7	2 1 5 6	syl3anc	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ≠ ∅ )
8		sorpsscmpl	⊢ ( [⊊] Or 𝐵 → [⊊] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } )
9	8	ad2antll	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → [⊊] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } )
10		fin2i	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ⊆ 𝒫 𝐴 ) ∧ ( { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ≠ ∅ ∧ [⊊] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ) ) → ∪ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } )
11	2 4 7 9 10	syl22anc	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → ∪ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } )
12		sorpssuni	⊢ ( [⊊] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } → ( ∃ 𝑚 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ∀ 𝑛 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝑚 ⊊ 𝑛 ↔ ∪ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ) )
13	9 12	syl	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → ( ∃ 𝑚 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ∀ 𝑛 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝑚 ⊊ 𝑛 ↔ ∪ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ) )
14	11 13	mpbird	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → ∃ 𝑚 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ∀ 𝑛 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝑚 ⊊ 𝑛 )
15		psseq2	⊢ ( 𝑧 = ( 𝐴 ∖ 𝑚 ) → ( 𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ ( 𝐴 ∖ 𝑚 ) ) )
16		psseq2	⊢ ( 𝑛 = ( 𝐴 ∖ 𝑤 ) → ( 𝑚 ⊊ 𝑛 ↔ 𝑚 ⊊ ( 𝐴 ∖ 𝑤 ) ) )
17		pssdifcom2	⊢ ( ( 𝑚 ⊆ 𝐴 ∧ 𝑤 ⊆ 𝐴 ) → ( 𝑤 ⊊ ( 𝐴 ∖ 𝑚 ) ↔ 𝑚 ⊊ ( 𝐴 ∖ 𝑤 ) ) )
18	15 16 17	fin23lem11	⊢ ( 𝐵 ⊆ 𝒫 𝐴 → ( ∃ 𝑚 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ∀ 𝑛 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑐 ) ∈ 𝐵 } ¬ 𝑚 ⊊ 𝑛 → ∃ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 ⊊ 𝑧 ) )
19	1 14 18	sylc	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → ∃ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 ⊊ 𝑧 )
20		sorpssint	⊢ ( [⊊] Or 𝐵 → ( ∃ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 ⊊ 𝑧 ↔ ∩ 𝐵 ∈ 𝐵 ) )
21	20	ad2antll	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → ( ∃ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 ⊊ 𝑧 ↔ ∩ 𝐵 ∈ 𝐵 ) )
22	19 21	mpbid	⊢ ( ( ( 𝐴 ∈ Fin^II ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → ∩ 𝐵 ∈ 𝐵 )

Metamath Proof Explorer

Theorem fin2i2

Proof