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 ∈ V a ≠ N ∧ x = a N
cusgrfi.f ⊢ F = x ∈ V ∖ N ⟼ x N
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 ∈ V a ≠ N ∧ x = a N
3 cusgrfi.f ⊢ F = x ∈ V ∖ N ⟼ x N
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 ⟼ x N ∈ V
15 13 14 mp1i ⊢ N ∈ V → x ∈ V ∖ N ⟼ x N ∈ V
16 3 15 eqeltrid ⊢ N ∈ V → F ∈ V
17 1 2 3 cusgrfilem2 ⊢ N ∈ V → F : V ∖ N ⟶ 1-1 onto P
18 f1oeq1 ⊢ f = F → f : V ∖ N ⟶ 1-1 onto P ↔ F : V ∖ N ⟶ 1-1 onto P
19 16 17 18 spcedv ⊢ N ∈ V → ∃ f f : V ∖ N ⟶ 1-1 onto P
20 bren ⊢ V ∖ N ≈ P ↔ ∃ f f : V ∖ N ⟶ 1-1 onto P
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