Metamath Proof Explorer

Theorem fin12

Description: Weak theorem which skips Ia but has a trivial proof, needed to prove fin1a2 . (Contributed by Stefan O'Rear, 8-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin12 ⊢A∈Fin→A∈FinII

Proof

Step Hyp Ref Expression
1 vex ⊢b∈V
2 1 a1i ⊢A∈Fin∧b∈𝒫𝒫A∧b≠∅∧[⊂]Orb→b∈V
3 isfin1-3 ⊢A∈Fin→A∈Fin↔[⊂]-1Fr𝒫A
4 3 ibi ⊢A∈Fin→[⊂]-1Fr𝒫A
5 4 ad2antrr ⊢A∈Fin∧b∈𝒫𝒫A∧b≠∅∧[⊂]Orb→[⊂]-1Fr𝒫A
6 elpwi ⊢b∈𝒫𝒫A→b⊆𝒫A
7 6 ad2antlr ⊢A∈Fin∧b∈𝒫𝒫A∧b≠∅∧[⊂]Orb→b⊆𝒫A
8 simprl ⊢A∈Fin∧b∈𝒫𝒫A∧b≠∅∧[⊂]Orb→b≠∅
9 fri ⊢b∈V∧[⊂]-1Fr𝒫A∧b⊆𝒫A∧b≠∅→∃c∈b∀d∈b¬d[⊂]-1c
10 2 5 7 8 9 syl22anc ⊢A∈Fin∧b∈𝒫𝒫A∧b≠∅∧[⊂]Orb→∃c∈b∀d∈b¬d[⊂]-1c
11 vex ⊢d∈V
12 vex ⊢c∈V
13 11 12 brcnv ⊢d[⊂]-1c↔c[⊂]d
14 11 brrpss ⊢c[⊂]d↔c⊂d
15 13 14 bitri ⊢d[⊂]-1c↔c⊂d
16 15 notbii ⊢¬d[⊂]-1c↔¬c⊂d
17 16 ralbii ⊢∀d∈b¬d[⊂]-1c↔∀d∈b¬c⊂d
18 17 rexbii ⊢∃c∈b∀d∈b¬d[⊂]-1c↔∃c∈b∀d∈b¬c⊂d
19 10 18 sylib ⊢A∈Fin∧b∈𝒫𝒫A∧b≠∅∧[⊂]Orb→∃c∈b∀d∈b¬c⊂d
20 sorpssuni ⊢[⊂]Orb→∃c∈b∀d∈b¬c⊂d↔⋃b∈b
21 20 ad2antll ⊢A∈Fin∧b∈𝒫𝒫A∧b≠∅∧[⊂]Orb→∃c∈b∀d∈b¬c⊂d↔⋃b∈b
22 19 21 mpbid ⊢A∈Fin∧b∈𝒫𝒫A∧b≠∅∧[⊂]Orb→⋃b∈b
23 22 ex ⊢A∈Fin∧b∈𝒫𝒫A→b≠∅∧[⊂]Orb→⋃b∈b
24 23 ralrimiva ⊢A∈Fin→∀b∈𝒫𝒫Ab≠∅∧[⊂]Orb→⋃b∈b
25 isfin2 ⊢A∈Fin→A∈FinII↔∀b∈𝒫𝒫Ab≠∅∧[⊂]Orb→⋃b∈b
26 24 25 mpbird ⊢A∈Fin→A∈FinII