Metamath Proof Explorer

Theorem cusgrfilem2

Description: Lemma 2 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 cusgrfilem2 ⊢ N ∈ V → F : V ∖ N ⟶ 1-1 onto P

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 eldifi ⊢ x ∈ V ∖ N → x ∈ V
5 id ⊢ N ∈ V → N ∈ V
6 prelpwi ⊢ x ∈ V ∧ N ∈ V → x N ∈ 𝒫 V
7 4 5 6 syl2anr ⊢ N ∈ V ∧ x ∈ V ∖ N → x N ∈ 𝒫 V
8 4 adantl ⊢ N ∈ V ∧ x ∈ V ∖ N → x ∈ V
9 eldifsni ⊢ x ∈ V ∖ N → x ≠ N
10 9 adantl ⊢ N ∈ V ∧ x ∈ V ∖ N → x ≠ N
11 eqidd ⊢ N ∈ V ∧ x ∈ V ∖ N → x N = x N
12 10 11 jca ⊢ N ∈ V ∧ x ∈ V ∖ N → x ≠ N ∧ x N = x N
13 id ⊢ x ∈ V → x ∈ V
14 neeq1 ⊢ a = x → a ≠ N ↔ x ≠ N
15 preq1 ⊢ a = x → a N = x N
16 15 eqeq2d ⊢ a = x → x N = a N ↔ x N = x N
17 14 16 anbi12d ⊢ a = x → a ≠ N ∧ x N = a N ↔ x ≠ N ∧ x N = x N
18 17 adantl ⊢ x ∈ V ∧ a = x → a ≠ N ∧ x N = a N ↔ x ≠ N ∧ x N = x N
19 13 18 rspcedv ⊢ x ∈ V → x ≠ N ∧ x N = x N → ∃ a ∈ V a ≠ N ∧ x N = a N
20 8 12 19 sylc ⊢ N ∈ V ∧ x ∈ V ∖ N → ∃ a ∈ V a ≠ N ∧ x N = a N
21 2 eleq2i ⊢ x N ∈ P ↔ x N ∈ x ∈ 𝒫 V | ∃ a ∈ V a ≠ N ∧ x = a N
22 eqeq1 ⊢ v = x N → v = a N ↔ x N = a N
23 22 anbi2d ⊢ v = x N → a ≠ N ∧ v = a N ↔ a ≠ N ∧ x N = a N
24 23 rexbidv ⊢ v = x N → ∃ a ∈ V a ≠ N ∧ v = a N ↔ ∃ a ∈ V a ≠ N ∧ x N = a N
25 eqeq1 ⊢ x = v → x = a N ↔ v = a N
26 25 anbi2d ⊢ x = v → a ≠ N ∧ x = a N ↔ a ≠ N ∧ v = a N
27 26 rexbidv ⊢ x = v → ∃ a ∈ V a ≠ N ∧ x = a N ↔ ∃ a ∈ V a ≠ N ∧ v = a N
28 27 cbvrabv ⊢ x ∈ 𝒫 V | ∃ a ∈ V a ≠ N ∧ x = a N = v ∈ 𝒫 V | ∃ a ∈ V a ≠ N ∧ v = a N
29 24 28 elrab2 ⊢ x N ∈ x ∈ 𝒫 V | ∃ a ∈ V a ≠ N ∧ x = a N ↔ x N ∈ 𝒫 V ∧ ∃ a ∈ V a ≠ N ∧ x N = a N
30 21 29 bitri ⊢ x N ∈ P ↔ x N ∈ 𝒫 V ∧ ∃ a ∈ V a ≠ N ∧ x N = a N
31 7 20 30 sylanbrc ⊢ N ∈ V ∧ x ∈ V ∖ N → x N ∈ P
32 31 ralrimiva ⊢ N ∈ V → ∀ x ∈ V ∖ N x N ∈ P
33 simpl ⊢ a ≠ N ∧ e = a N → a ≠ N
34 33 anim2i ⊢ a ∈ V ∧ a ≠ N ∧ e = a N → a ∈ V ∧ a ≠ N
35 34 adantl ⊢ N ∈ V ∧ e ∈ 𝒫 V ∧ a ∈ V ∧ a ≠ N ∧ e = a N → a ∈ V ∧ a ≠ N
36 eldifsn ⊢ a ∈ V ∖ N ↔ a ∈ V ∧ a ≠ N
37 35 36 sylibr ⊢ N ∈ V ∧ e ∈ 𝒫 V ∧ a ∈ V ∧ a ≠ N ∧ e = a N → a ∈ V ∖ N
38 eqeq1 ⊢ e = a N → e = x N ↔ a N = x N
39 38 adantl ⊢ a ≠ N ∧ e = a N → e = x N ↔ a N = x N
40 39 ad2antlr ⊢ a ∈ V ∧ a ≠ N ∧ e = a N ∧ x ∈ V ∖ N → e = x N ↔ a N = x N
41 vex ⊢ a ∈ V
42 vex ⊢ x ∈ V
43 41 42 preqr1 ⊢ a N = x N → a = x
44 43 equcomd ⊢ a N = x N → x = a
45 40 44 biimtrdi ⊢ a ∈ V ∧ a ≠ N ∧ e = a N ∧ x ∈ V ∖ N → e = x N → x = a
46 45 adantll ⊢ N ∈ V ∧ e ∈ 𝒫 V ∧ a ∈ V ∧ a ≠ N ∧ e = a N ∧ x ∈ V ∖ N → e = x N → x = a
47 15 equcoms ⊢ x = a → a N = x N
48 47 eqeq2d ⊢ x = a → e = a N ↔ e = x N
49 48 biimpcd ⊢ e = a N → x = a → e = x N
50 49 adantl ⊢ a ≠ N ∧ e = a N → x = a → e = x N
51 50 adantl ⊢ a ∈ V ∧ a ≠ N ∧ e = a N → x = a → e = x N
52 51 ad2antlr ⊢ N ∈ V ∧ e ∈ 𝒫 V ∧ a ∈ V ∧ a ≠ N ∧ e = a N ∧ x ∈ V ∖ N → x = a → e = x N
53 46 52 impbid ⊢ N ∈ V ∧ e ∈ 𝒫 V ∧ a ∈ V ∧ a ≠ N ∧ e = a N ∧ x ∈ V ∖ N → e = x N ↔ x = a
54 53 ralrimiva ⊢ N ∈ V ∧ e ∈ 𝒫 V ∧ a ∈ V ∧ a ≠ N ∧ e = a N → ∀ x ∈ V ∖ N e = x N ↔ x = a
55 37 54 jca ⊢ N ∈ V ∧ e ∈ 𝒫 V ∧ a ∈ V ∧ a ≠ N ∧ e = a N → a ∈ V ∖ N ∧ ∀ x ∈ V ∖ N e = x N ↔ x = a
56 55 ex ⊢ N ∈ V ∧ e ∈ 𝒫 V → a ∈ V ∧ a ≠ N ∧ e = a N → a ∈ V ∖ N ∧ ∀ x ∈ V ∖ N e = x N ↔ x = a
57 56 reximdv2 ⊢ N ∈ V ∧ e ∈ 𝒫 V → ∃ a ∈ V a ≠ N ∧ e = a N → ∃ a ∈ V ∖ N ∀ x ∈ V ∖ N e = x N ↔ x = a
58 57 expimpd ⊢ N ∈ V → e ∈ 𝒫 V ∧ ∃ a ∈ V a ≠ N ∧ e = a N → ∃ a ∈ V ∖ N ∀ x ∈ V ∖ N e = x N ↔ x = a
59 eqeq1 ⊢ x = e → x = a N ↔ e = a N
60 59 anbi2d ⊢ x = e → a ≠ N ∧ x = a N ↔ a ≠ N ∧ e = a N
61 60 rexbidv ⊢ x = e → ∃ a ∈ V a ≠ N ∧ x = a N ↔ ∃ a ∈ V a ≠ N ∧ e = a N
62 61 2 elrab2 ⊢ e ∈ P ↔ e ∈ 𝒫 V ∧ ∃ a ∈ V a ≠ N ∧ e = a N
63 reu6 ⊢ ∃! x ∈ V ∖ N e = x N ↔ ∃ a ∈ V ∖ N ∀ x ∈ V ∖ N e = x N ↔ x = a
64 58 62 63 3imtr4g ⊢ N ∈ V → e ∈ P → ∃! x ∈ V ∖ N e = x N
65 64 ralrimiv ⊢ N ∈ V → ∀ e ∈ P ∃! x ∈ V ∖ N e = x N
66 3 f1ompt ⊢ F : V ∖ N ⟶ 1-1 onto P ↔ ∀ x ∈ V ∖ N x N ∈ P ∧ ∀ e ∈ P ∃! x ∈ V ∖ N e = x N
67 32 65 66 sylanbrc ⊢ N ∈ V → F : V ∖ N ⟶ 1-1 onto P