Metamath Proof Explorer

Theorem cusgrfilem3

Description: Lemma 3 for cusgrfi . (Contributed by Alexander van der Vekens, 13-Jan-2018) (Revised by AV, 11-Nov-2020)

Ref Expression
Hypotheses cusgrfi.v ⊢V=Vtx⁡G
cusgrfi.p ⊢P=x∈𝒫V|∃a∈Va≠N∧x=aN
cusgrfi.f ⊢F=x∈V∖N⟼xN
Assertion cusgrfilem3 ⊢N∈V→V∈Fin↔P∈Fin

Proof

Step Hyp Ref Expression
1 cusgrfi.v ⊢V=Vtx⁡G
2 cusgrfi.p ⊢P=x∈𝒫V|∃a∈Va≠N∧x=aN
3 cusgrfi.f ⊢F=x∈V∖N⟼xN
4 diffi ⊢V∈Fin→V∖N∈Fin
5 simpr ⊢N∈V∧¬V∈Fin→¬V∈Fin
6 snfi ⊢N∈Fin
7 difinf ⊢¬V∈Fin∧N∈Fin→¬V∖N∈Fin
8 5 6 7 sylancl ⊢N∈V∧¬V∈Fin→¬V∖N∈Fin
9 8 ex ⊢N∈V→¬V∈Fin→¬V∖N∈Fin
10 9 con4d ⊢N∈V→V∖N∈Fin→V∈Fin
11 4 10 impbid2 ⊢N∈V→V∈Fin↔V∖N∈Fin
12 1 fvexi ⊢V∈V
13 12 difexi ⊢V∖N∈V
14 mptexg ⊢V∖N∈V→x∈V∖N⟼xN∈V
15 13 14 mp1i ⊢N∈V→x∈V∖N⟼xN∈V
16 3 15 eqeltrid ⊢N∈V→F∈V
17 1 2 3 cusgrfilem2 ⊢N∈V→F:V∖N⟶1-1 ontoP
18 f1oeq1 ⊢f=F→f:V∖N⟶1-1 ontoP↔F:V∖N⟶1-1 ontoP
19 16 17 18 spcedv ⊢N∈V→∃ff:V∖N⟶1-1 ontoP
20 bren ⊢V∖N≈P↔∃ff:V∖N⟶1-1 ontoP
21 19 20 sylibr ⊢N∈V→V∖N≈P
22 enfi ⊢V∖N≈P→V∖N∈Fin↔P∈Fin
23 21 22 syl ⊢N∈V→V∖N∈Fin↔P∈Fin
24 11 23 bitrd ⊢N∈V→V∈Fin↔P∈Fin