Metamath Proof Explorer

Theorem isfin2-2

Description: Fin2 expressed in terms of minimal elements. (Contributed by Stefan O'Rear, 2-Nov-2014) (Proof shortened by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion isfin2-2 ⊢ A ∈ V → A ∈ FinII ↔ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y

Proof

Step Hyp Ref Expression
1 elpwi ⊢ y ∈ 𝒫 𝒫 A → y ⊆ 𝒫 A
2 fin2i2 ⊢ A ∈ FinII ∧ y ⊆ 𝒫 A ∧ y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y
3 2 ex ⊢ A ∈ FinII ∧ y ⊆ 𝒫 A → y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y
4 1 3 sylan2 ⊢ A ∈ FinII ∧ y ∈ 𝒫 𝒫 A → y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y
5 4 ralrimiva ⊢ A ∈ FinII → ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y
6 elpwi ⊢ b ∈ 𝒫 𝒫 A → b ⊆ 𝒫 A
7 simp1r ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → b ⊆ 𝒫 A
8 simp1l ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → A ∈ V
9 simp3l ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → b ≠ ∅
10 fin23lem7 ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ b ≠ ∅ → c ∈ 𝒫 A | A ∖ c ∈ b ≠ ∅
11 8 7 9 10 syl3anc ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → c ∈ 𝒫 A | A ∖ c ∈ b ≠ ∅
12 sorpsscmpl ⊢ [⊂] Or b → [⊂] Or c ∈ 𝒫 A | A ∖ c ∈ b
13 12 adantl ⊢ b ≠ ∅ ∧ [⊂] Or b → [⊂] Or c ∈ 𝒫 A | A ∖ c ∈ b
14 13 3ad2ant3 ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → [⊂] Or c ∈ 𝒫 A | A ∖ c ∈ b
15 neeq1 ⊢ y = c ∈ 𝒫 A | A ∖ c ∈ b → y ≠ ∅ ↔ c ∈ 𝒫 A | A ∖ c ∈ b ≠ ∅
16 soeq2 ⊢ y = c ∈ 𝒫 A | A ∖ c ∈ b → [⊂] Or y ↔ [⊂] Or c ∈ 𝒫 A | A ∖ c ∈ b
17 15 16 anbi12d ⊢ y = c ∈ 𝒫 A | A ∖ c ∈ b → y ≠ ∅ ∧ [⊂] Or y ↔ c ∈ 𝒫 A | A ∖ c ∈ b ≠ ∅ ∧ [⊂] Or c ∈ 𝒫 A | A ∖ c ∈ b
18 inteq ⊢ y = c ∈ 𝒫 A | A ∖ c ∈ b → ⋂ y = ⋂ c ∈ 𝒫 A | A ∖ c ∈ b
19 id ⊢ y = c ∈ 𝒫 A | A ∖ c ∈ b → y = c ∈ 𝒫 A | A ∖ c ∈ b
20 18 19 eleq12d ⊢ y = c ∈ 𝒫 A | A ∖ c ∈ b → ⋂ y ∈ y ↔ ⋂ c ∈ 𝒫 A | A ∖ c ∈ b ∈ c ∈ 𝒫 A | A ∖ c ∈ b
21 17 20 imbi12d ⊢ y = c ∈ 𝒫 A | A ∖ c ∈ b → y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ↔ c ∈ 𝒫 A | A ∖ c ∈ b ≠ ∅ ∧ [⊂] Or c ∈ 𝒫 A | A ∖ c ∈ b → ⋂ c ∈ 𝒫 A | A ∖ c ∈ b ∈ c ∈ 𝒫 A | A ∖ c ∈ b
22 simp2 ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y
23 ssrab2 ⊢ c ∈ 𝒫 A | A ∖ c ∈ b ⊆ 𝒫 A
24 pwexg ⊢ A ∈ V → 𝒫 A ∈ V
25 elpw2g ⊢ 𝒫 A ∈ V → c ∈ 𝒫 A | A ∖ c ∈ b ∈ 𝒫 𝒫 A ↔ c ∈ 𝒫 A | A ∖ c ∈ b ⊆ 𝒫 A
26 8 24 25 3syl ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → c ∈ 𝒫 A | A ∖ c ∈ b ∈ 𝒫 𝒫 A ↔ c ∈ 𝒫 A | A ∖ c ∈ b ⊆ 𝒫 A
27 23 26 mpbiri ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → c ∈ 𝒫 A | A ∖ c ∈ b ∈ 𝒫 𝒫 A
28 21 22 27 rspcdva ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → c ∈ 𝒫 A | A ∖ c ∈ b ≠ ∅ ∧ [⊂] Or c ∈ 𝒫 A | A ∖ c ∈ b → ⋂ c ∈ 𝒫 A | A ∖ c ∈ b ∈ c ∈ 𝒫 A | A ∖ c ∈ b
29 11 14 28 mp2and ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → ⋂ c ∈ 𝒫 A | A ∖ c ∈ b ∈ c ∈ 𝒫 A | A ∖ c ∈ b
30 sorpssint ⊢ [⊂] Or c ∈ 𝒫 A | A ∖ c ∈ b → ∃ z ∈ c ∈ 𝒫 A | A ∖ c ∈ b ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ b ¬ w ⊂ z ↔ ⋂ c ∈ 𝒫 A | A ∖ c ∈ b ∈ c ∈ 𝒫 A | A ∖ c ∈ b
31 14 30 syl ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → ∃ z ∈ c ∈ 𝒫 A | A ∖ c ∈ b ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ b ¬ w ⊂ z ↔ ⋂ c ∈ 𝒫 A | A ∖ c ∈ b ∈ c ∈ 𝒫 A | A ∖ c ∈ b
32 29 31 mpbird ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → ∃ z ∈ c ∈ 𝒫 A | A ∖ c ∈ b ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ b ¬ w ⊂ z
33 psseq1 ⊢ m = A ∖ z → m ⊂ n ↔ A ∖ z ⊂ n
34 psseq1 ⊢ w = A ∖ n → w ⊂ z ↔ A ∖ n ⊂ z
35 pssdifcom1 ⊢ z ⊆ A ∧ n ⊆ A → A ∖ z ⊂ n ↔ A ∖ n ⊂ z
36 33 34 35 fin23lem11 ⊢ b ⊆ 𝒫 A → ∃ z ∈ c ∈ 𝒫 A | A ∖ c ∈ b ∀ w ∈ c ∈ 𝒫 A | A ∖ c ∈ b ¬ w ⊂ z → ∃ m ∈ b ∀ n ∈ b ¬ m ⊂ n
37 7 32 36 sylc ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → ∃ m ∈ b ∀ n ∈ b ¬ m ⊂ n
38 simp3r ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → [⊂] Or b
39 sorpssuni ⊢ [⊂] Or b → ∃ m ∈ b ∀ n ∈ b ¬ m ⊂ n ↔ ⋃ b ∈ b
40 38 39 syl ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → ∃ m ∈ b ∀ n ∈ b ¬ m ⊂ n ↔ ⋃ b ∈ b
41 37 40 mpbid ⊢ A ∈ V ∧ b ⊆ 𝒫 A ∧ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y ∧ b ≠ ∅ ∧ [⊂] Or b → ⋃ b ∈ b
42 41 3exp ⊢ A ∈ V ∧ b ⊆ 𝒫 A → ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y → b ≠ ∅ ∧ [⊂] Or b → ⋃ b ∈ b
43 6 42 sylan2 ⊢ A ∈ V ∧ b ∈ 𝒫 𝒫 A → ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y → b ≠ ∅ ∧ [⊂] Or b → ⋃ b ∈ b
44 43 ralrimdva ⊢ A ∈ V → ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y → ∀ b ∈ 𝒫 𝒫 A b ≠ ∅ ∧ [⊂] Or b → ⋃ b ∈ b
45 isfin2 ⊢ A ∈ V → A ∈ FinII ↔ ∀ b ∈ 𝒫 𝒫 A b ≠ ∅ ∧ [⊂] Or b → ⋃ b ∈ b
46 44 45 sylibrd ⊢ A ∈ V → ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y → A ∈ FinII
47 5 46 impbid2 ⊢ A ∈ V → A ∈ FinII ↔ ∀ y ∈ 𝒫 𝒫 A y ≠ ∅ ∧ [⊂] Or y → ⋂ y ∈ y