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∈Va≠N∧x=aN
cusgrfi.f ⊢F=x∈V∖N⟼xN
Assertion cusgrfilem2 ⊢N∈V→F:V∖N⟶1-1 ontoP

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