Metamath Proof Explorer


Theorem isomuspgrlem2d

Description: Lemma 4 for isomuspgrlem2 . (Contributed by AV, 1-Dec-2022)

Ref Expression
Hypotheses isomushgr.v V = Vtx A
isomushgr.w W = Vtx B
isomushgr.e E = Edg A
isomushgr.k K = Edg B
isomuspgrlem2.g G = x E F x
isomuspgrlem2.a φ A USHGraph
isomuspgrlem2.f φ F : V 1-1 onto W
isomuspgrlem2.i φ a V b V a b E F a F b K
isomuspgrlem2.x φ F X
isomuspgrlem2.b φ B USHGraph
Assertion isomuspgrlem2d φ G : E onto K

Proof

Step Hyp Ref Expression
1 isomushgr.v V = Vtx A
2 isomushgr.w W = Vtx B
3 isomushgr.e E = Edg A
4 isomushgr.k K = Edg B
5 isomuspgrlem2.g G = x E F x
6 isomuspgrlem2.a φ A USHGraph
7 isomuspgrlem2.f φ F : V 1-1 onto W
8 isomuspgrlem2.i φ a V b V a b E F a F b K
9 isomuspgrlem2.x φ F X
10 isomuspgrlem2.b φ B USHGraph
11 1 2 3 4 5 6 7 8 isomuspgrlem2b φ G : E K
12 uspgrupgr B USHGraph B UPGraph
13 10 12 syl φ B UPGraph
14 2 4 upgredg B UPGraph y K c W d W y = c d
15 13 14 sylan φ y K c W d W y = c d
16 eleq1 y = c d y K c d K
17 16 anbi2d y = c d φ y K φ c d K
18 f1ofo F : V 1-1 onto W F : V onto W
19 7 18 syl φ F : V onto W
20 foelrn F : V onto W c W m V c = F m
21 19 20 sylan φ c W m V c = F m
22 21 ex φ c W m V c = F m
23 foelrn F : V onto W d W n V d = F n
24 19 23 sylan φ d W n V d = F n
25 24 ex φ d W n V d = F n
26 22 25 anim12d φ c W d W m V c = F m n V d = F n
27 26 adantr φ c d K c W d W m V c = F m n V d = F n
28 27 imp φ c d K c W d W m V c = F m n V d = F n
29 preq12 c = F m d = F n c d = F m F n
30 29 ancoms d = F n c = F m c d = F m F n
31 30 eleq1d d = F n c = F m c d K F m F n K
32 preq1 a = m a b = m b
33 32 eleq1d a = m a b E m b E
34 fveq2 a = m F a = F m
35 34 preq1d a = m F a F b = F m F b
36 35 eleq1d a = m F a F b K F m F b K
37 33 36 bibi12d a = m a b E F a F b K m b E F m F b K
38 preq2 b = n m b = m n
39 38 eleq1d b = n m b E m n E
40 fveq2 b = n F b = F n
41 40 preq2d b = n F m F b = F m F n
42 41 eleq1d b = n F m F b K F m F n K
43 39 42 bibi12d b = n m b E F m F b K m n E F m F n K
44 37 43 rspc2va m V n V a V b V a b E F a F b K m n E F m F n K
45 44 bicomd m V n V a V b V a b E F a F b K F m F n K m n E
46 45 ancoms a V b V a b E F a F b K m V n V F m F n K m n E
47 46 biimpd a V b V a b E F a F b K m V n V F m F n K m n E
48 47 ex a V b V a b E F a F b K m V n V F m F n K m n E
49 8 48 syl φ m V n V F m F n K m n E
50 49 com13 F m F n K m V n V φ m n E
51 31 50 syl6bi d = F n c = F m c d K m V n V φ m n E
52 51 com14 φ c d K m V n V d = F n c = F m m n E
53 52 imp φ c d K m V n V d = F n c = F m m n E
54 53 adantr φ c d K c W d W m V n V d = F n c = F m m n E
55 54 imp31 φ c d K c W d W m V n V d = F n c = F m m n E
56 imaeq2 e = m n F e = F m n
57 f1ofn F : V 1-1 onto W F Fn V
58 7 57 syl φ F Fn V
59 58 ad3antrrr φ c d K c W d W m V n V F Fn V
60 simprl φ c d K c W d W m V n V m V
61 simpr m V n V n V
62 61 adantl φ c d K c W d W m V n V n V
63 59 60 62 3jca φ c d K c W d W m V n V F Fn V m V n V
64 63 adantr φ c d K c W d W m V n V d = F n c = F m F Fn V m V n V
65 fnimapr F Fn V m V n V F m n = F m F n
66 64 65 syl φ c d K c W d W m V n V d = F n c = F m F m n = F m F n
67 56 66 sylan9eqr φ c d K c W d W m V n V d = F n c = F m e = m n F e = F m F n
68 67 eqeq2d φ c d K c W d W m V n V d = F n c = F m e = m n c d = F e c d = F m F n
69 30 adantl φ c d K c W d W m V n V d = F n c = F m c d = F m F n
70 55 68 69 rspcedvd φ c d K c W d W m V n V d = F n c = F m e E c d = F e
71 70 ex φ c d K c W d W m V n V d = F n c = F m e E c d = F e
72 71 anassrs φ c d K c W d W m V n V d = F n c = F m e E c d = F e
73 72 expd φ c d K c W d W m V n V d = F n c = F m e E c d = F e
74 73 rexlimdva φ c d K c W d W m V n V d = F n c = F m e E c d = F e
75 74 com23 φ c d K c W d W m V c = F m n V d = F n e E c d = F e
76 75 rexlimdva φ c d K c W d W m V c = F m n V d = F n e E c d = F e
77 76 impd φ c d K c W d W m V c = F m n V d = F n e E c d = F e
78 28 77 mpd φ c d K c W d W e E c d = F e
79 78 ex φ c d K c W d W e E c d = F e
80 17 79 syl6bi y = c d φ y K c W d W e E c d = F e
81 80 impd y = c d φ y K c W d W e E c d = F e
82 81 impcom φ y K c W d W y = c d e E c d = F e
83 simpr φ y K c W d W y = c d y = c d
84 83 adantr φ y K c W d W y = c d e E y = c d
85 9 ad4antr φ y K c W d W y = c d e E F X
86 1 2 3 4 5 isomuspgrlem2a F X y E F y = G y
87 85 86 syl φ y K c W d W y = c d e E y E F y = G y
88 imaeq2 y = e F y = F e
89 fveq2 y = e G y = G e
90 88 89 eqeq12d y = e F y = G y F e = G e
91 90 rspcv e E y E F y = G y F e = G e
92 eqcom G e = F e F e = G e
93 91 92 syl6ibr e E y E F y = G y G e = F e
94 93 adantl φ y K c W d W y = c d e E y E F y = G y G e = F e
95 87 94 mpd φ y K c W d W y = c d e E G e = F e
96 84 95 eqeq12d φ y K c W d W y = c d e E y = G e c d = F e
97 96 rexbidva φ y K c W d W y = c d e E y = G e e E c d = F e
98 82 97 mpbird φ y K c W d W y = c d e E y = G e
99 98 ex φ y K c W d W y = c d e E y = G e
100 99 rexlimdvva φ y K c W d W y = c d e E y = G e
101 15 100 mpd φ y K e E y = G e
102 101 ralrimiva φ y K e E y = G e
103 dffo3 G : E onto K G : E K y K e E y = G e
104 11 102 103 sylanbrc φ G : E onto K