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∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y

Proof

Step Hyp Ref Expression
1 elpwi ⊢y∈𝒫𝒫A→y⊆𝒫A
2 fin2i2 ⊢A∈FinII∧y⊆𝒫A∧y≠∅∧[⊂]Ory→⋂y∈y
3 2 ex ⊢A∈FinII∧y⊆𝒫A→y≠∅∧[⊂]Ory→⋂y∈y
4 1 3 sylan2 ⊢A∈FinII∧y∈𝒫𝒫A→y≠∅∧[⊂]Ory→⋂y∈y
5 4 ralrimiva ⊢A∈FinII→∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y
6 elpwi ⊢b∈𝒫𝒫A→b⊆𝒫A
7 simp1r ⊢A∈V∧b⊆𝒫A∧∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→b⊆𝒫A
8 simp1l ⊢A∈V∧b⊆𝒫A∧∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→A∈V
9 simp3l ⊢A∈V∧b⊆𝒫A∧∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→b≠∅
10 fin23lem7 ⊢A∈V∧b⊆𝒫A∧b≠∅→c∈𝒫A|A∖c∈b≠∅
11 8 7 9 10 syl3anc ⊢A∈V∧b⊆𝒫A∧∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→c∈𝒫A|A∖c∈b≠∅
12 sorpsscmpl ⊢[⊂]Orb→[⊂]Orc∈𝒫A|A∖c∈b
13 12 adantl ⊢b≠∅∧[⊂]Orb→[⊂]Orc∈𝒫A|A∖c∈b
14 13 3ad2ant3 ⊢A∈V∧b⊆𝒫A∧∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→[⊂]Orc∈𝒫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→[⊂]Ory↔[⊂]Orc∈𝒫A|A∖c∈b
17 15 16 anbi12d ⊢y=c∈𝒫A|A∖c∈b→y≠∅∧[⊂]Ory↔c∈𝒫A|A∖c∈b≠∅∧[⊂]Orc∈𝒫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≠∅∧[⊂]Ory→⋂y∈y↔c∈𝒫A|A∖c∈b≠∅∧[⊂]Orc∈𝒫A|A∖c∈b→⋂c∈𝒫A|A∖c∈b∈c∈𝒫A|A∖c∈b
22 simp2 ⊢A∈V∧b⊆𝒫A∧∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂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∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→c∈𝒫A|A∖c∈b∈𝒫𝒫A↔c∈𝒫A|A∖c∈b⊆𝒫A
27 23 26 mpbiri ⊢A∈V∧b⊆𝒫A∧∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→c∈𝒫A|A∖c∈b∈𝒫𝒫A
28 21 22 27 rspcdva ⊢A∈V∧b⊆𝒫A∧∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→c∈𝒫A|A∖c∈b≠∅∧[⊂]Orc∈𝒫A|A∖c∈b→⋂c∈𝒫A|A∖c∈b∈c∈𝒫A|A∖c∈b
29 11 14 28 mp2and ⊢A∈V∧b⊆𝒫A∧∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→⋂c∈𝒫A|A∖c∈b∈c∈𝒫A|A∖c∈b
30 sorpssint ⊢[⊂]Orc∈𝒫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∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→∃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∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→∃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∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→∃m∈b∀n∈b¬m⊂n
38 simp3r ⊢A∈V∧b⊆𝒫A∧∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→[⊂]Orb
39 sorpssuni ⊢[⊂]Orb→∃m∈b∀n∈b¬m⊂n↔⋃b∈b
40 38 39 syl ⊢A∈V∧b⊆𝒫A∧∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→∃m∈b∀n∈b¬m⊂n↔⋃b∈b
41 37 40 mpbid ⊢A∈V∧b⊆𝒫A∧∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y∧b≠∅∧[⊂]Orb→⋃b∈b
42 41 3exp ⊢A∈V∧b⊆𝒫A→∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y→b≠∅∧[⊂]Orb→⋃b∈b
43 6 42 sylan2 ⊢A∈V∧b∈𝒫𝒫A→∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y→b≠∅∧[⊂]Orb→⋃b∈b
44 43 ralrimdva ⊢A∈V→∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y→∀b∈𝒫𝒫Ab≠∅∧[⊂]Orb→⋃b∈b
45 isfin2 ⊢A∈V→A∈FinII↔∀b∈𝒫𝒫Ab≠∅∧[⊂]Orb→⋃b∈b
46 44 45 sylibrd ⊢A∈V→∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y→A∈FinII
47 5 46 impbid2 ⊢A∈V→A∈FinII↔∀y∈𝒫𝒫Ay≠∅∧[⊂]Ory→⋂y∈y