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 syl6bi 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