Metamath Proof Explorer

Theorem fin2i2

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

Ref Expression
Assertion fin2i2 ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ ∧ [⊂] Or B → ⋂ B ∈ B

Proof

Step Hyp Ref Expression
1 simplr ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ ∧ [⊂] Or B → B ⊆ 𝒫 A
2 simpll ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ ∧ [⊂] Or B → A ∈ FinII
3 ssrab2 ⊢ c ∈ 𝒫 A | A ∖ c ∈ B ⊆ 𝒫 A
4 3 a1i ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ ∧ [⊂] Or B → c ∈ 𝒫 A | A ∖ c ∈ B ⊆ 𝒫 A
5 simprl ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ ∧ [⊂] Or B → B ≠ ∅
6 fin23lem7 ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ → c ∈ 𝒫 A | A ∖ c ∈ B ≠ ∅
7 2 1 5 6 syl3anc ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ ∧ [⊂] Or B → c ∈ 𝒫 A | A ∖ c ∈ B ≠ ∅
8 sorpsscmpl ⊢ [⊂] Or B → [⊂] Or c ∈ 𝒫 A | A ∖ c ∈ B
9 8 ad2antll ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ ∧ [⊂] Or B → [⊂] Or c ∈ 𝒫 A | A ∖ c ∈ B
10 fin2i ⊢ A ∈ FinII ∧ c ∈ 𝒫 A | A ∖ c ∈ B ⊆ 𝒫 A ∧ c ∈ 𝒫 A | A ∖ c ∈ B ≠ ∅ ∧ [⊂] Or c ∈ 𝒫 A | A ∖ c ∈ B → ⋃ c ∈ 𝒫 A | A ∖ c ∈ B ∈ c ∈ 𝒫 A | A ∖ c ∈ B
11 2 4 7 9 10 syl22anc ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ ∧ [⊂] Or B → ⋃ c ∈ 𝒫 A | A ∖ c ∈ B ∈ c ∈ 𝒫 A | A ∖ c ∈ B
12 sorpssuni ⊢ [⊂] Or c ∈ 𝒫 A | A ∖ c ∈ B → ∃ m ∈ c ∈ 𝒫 A | A ∖ c ∈ B ∀ n ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ m ⊂ n ↔ ⋃ c ∈ 𝒫 A | A ∖ c ∈ B ∈ c ∈ 𝒫 A | A ∖ c ∈ B
13 9 12 syl ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ ∧ [⊂] Or B → ∃ m ∈ c ∈ 𝒫 A | A ∖ c ∈ B ∀ n ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ m ⊂ n ↔ ⋃ c ∈ 𝒫 A | A ∖ c ∈ B ∈ c ∈ 𝒫 A | A ∖ c ∈ B
14 11 13 mpbird ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ ∧ [⊂] Or B → ∃ m ∈ c ∈ 𝒫 A | A ∖ c ∈ B ∀ n ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ m ⊂ n
15 psseq2 ⊢ z = A ∖ m → w ⊂ z ↔ w ⊂ A ∖ m
16 psseq2 ⊢ n = A ∖ w → m ⊂ n ↔ m ⊂ A ∖ w
17 pssdifcom2 ⊢ m ⊆ A ∧ w ⊆ A → w ⊂ A ∖ m ↔ m ⊂ A ∖ w
18 15 16 17 fin23lem11 ⊢ B ⊆ 𝒫 A → ∃ m ∈ c ∈ 𝒫 A | A ∖ c ∈ B ∀ n ∈ c ∈ 𝒫 A | A ∖ c ∈ B ¬ m ⊂ n → ∃ z ∈ B ∀ w ∈ B ¬ w ⊂ z
19 1 14 18 sylc ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ ∧ [⊂] Or B → ∃ z ∈ B ∀ w ∈ B ¬ w ⊂ z
20 sorpssint ⊢ [⊂] Or B → ∃ z ∈ B ∀ w ∈ B ¬ w ⊂ z ↔ ⋂ B ∈ B
21 20 ad2antll ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ ∧ [⊂] Or B → ∃ z ∈ B ∀ w ∈ B ¬ w ⊂ z ↔ ⋂ B ∈ B
22 19 21 mpbid ⊢ A ∈ FinII ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ ∧ [⊂] Or B → ⋂ B ∈ B