Metamath Proof Explorer

Theorem isuspgrimlem

Description: Lemma for isuspgrim . (Contributed by AV, 27-Apr-2025)

Ref Expression
Hypotheses isusgrim.v ⊢ V = Vtx ⁡ G
isusgrim.w ⊢ W = Vtx ⁡ H
isusgrim.e ⊢ E = Edg ⁡ G
isusgrim.d ⊢ D = Edg ⁡ H
Assertion isuspgrimlem ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → e ∈ E ⟼ F e : E ⟶ 1-1 onto D

Proof

Step Hyp Ref Expression
1 isusgrim.v ⊢ V = Vtx ⁡ G
2 isusgrim.w ⊢ W = Vtx ⁡ H
3 isusgrim.e ⊢ E = Edg ⁡ G
4 isusgrim.d ⊢ D = Edg ⁡ H
5 uspgrupgr ⊢ G ∈ USHGraph → G ∈ UPGraph
6 5 adantr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → G ∈ UPGraph
7 6 adantr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W → G ∈ UPGraph
8 7 adantr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → G ∈ UPGraph
9 1 3 upgredg ⊢ G ∈ UPGraph ∧ e ∈ E → ∃ a ∈ V ∃ b ∈ V e = a b
10 8 9 sylan ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ e ∈ E → ∃ a ∈ V ∃ b ∈ V e = a b
11 preq12 ⊢ x = a ∧ y = b → x y = a b
12 11 eleq1d ⊢ x = a ∧ y = b → x y ∈ E ↔ a b ∈ E
13 fveq2 ⊢ x = a → F ⁡ x = F ⁡ a
14 13 adantr ⊢ x = a ∧ y = b → F ⁡ x = F ⁡ a
15 fveq2 ⊢ y = b → F ⁡ y = F ⁡ b
16 15 adantl ⊢ x = a ∧ y = b → F ⁡ y = F ⁡ b
17 14 16 preq12d ⊢ x = a ∧ y = b → F ⁡ x F ⁡ y = F ⁡ a F ⁡ b
18 17 eleq1d ⊢ x = a ∧ y = b → F ⁡ x F ⁡ y ∈ D ↔ F ⁡ a F ⁡ b ∈ D
19 12 18 bibi12d ⊢ x = a ∧ y = b → x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ↔ a b ∈ E ↔ F ⁡ a F ⁡ b ∈ D
20 19 rspc2gv ⊢ a ∈ V ∧ b ∈ V → ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → a b ∈ E ↔ F ⁡ a F ⁡ b ∈ D
21 20 com12 ⊢ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → a ∈ V ∧ b ∈ V → a b ∈ E ↔ F ⁡ a F ⁡ b ∈ D
22 21 adantl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → a ∈ V ∧ b ∈ V → a b ∈ E ↔ F ⁡ a F ⁡ b ∈ D
23 22 imp ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ V ∧ b ∈ V → a b ∈ E ↔ F ⁡ a F ⁡ b ∈ D
24 f1ofn ⊢ F : V ⟶ 1-1 onto W → F Fn V
25 24 ad3antlr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ V ∧ b ∈ V → F Fn V
26 simprl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ V ∧ b ∈ V → a ∈ V
27 simpr ⊢ a ∈ V ∧ b ∈ V → b ∈ V
28 27 adantl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ V ∧ b ∈ V → b ∈ V
29 fnimapr ⊢ F Fn V ∧ a ∈ V ∧ b ∈ V → F a b = F ⁡ a F ⁡ b
30 25 26 28 29 syl3anc ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ V ∧ b ∈ V → F a b = F ⁡ a F ⁡ b
31 30 eqcomd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ V ∧ b ∈ V → F ⁡ a F ⁡ b = F a b
32 31 eleq1d ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ V ∧ b ∈ V → F ⁡ a F ⁡ b ∈ D ↔ F a b ∈ D
33 23 32 bitrd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ V ∧ b ∈ V → a b ∈ E ↔ F a b ∈ D
34 33 adantr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ V ∧ b ∈ V ∧ e = a b → a b ∈ E ↔ F a b ∈ D
35 34 biimpd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ V ∧ b ∈ V ∧ e = a b → a b ∈ E → F a b ∈ D
36 eleq1 ⊢ e = a b → e ∈ E ↔ a b ∈ E
37 imaeq2 ⊢ e = a b → F e = F a b
38 37 eleq1d ⊢ e = a b → F e ∈ D ↔ F a b ∈ D
39 36 38 imbi12d ⊢ e = a b → e ∈ E → F e ∈ D ↔ a b ∈ E → F a b ∈ D
40 39 adantl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ V ∧ b ∈ V ∧ e = a b → e ∈ E → F e ∈ D ↔ a b ∈ E → F a b ∈ D
41 35 40 mpbird ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ V ∧ b ∈ V ∧ e = a b → e ∈ E → F e ∈ D
42 41 exp31 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → a ∈ V ∧ b ∈ V → e = a b → e ∈ E → F e ∈ D
43 42 com23 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → e = a b → a ∈ V ∧ b ∈ V → e ∈ E → F e ∈ D
44 43 com24 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → e ∈ E → a ∈ V ∧ b ∈ V → e = a b → F e ∈ D
45 44 imp ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ e ∈ E → a ∈ V ∧ b ∈ V → e = a b → F e ∈ D
46 45 rexlimdvv ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ e ∈ E → ∃ a ∈ V ∃ b ∈ V e = a b → F e ∈ D
47 10 46 mpd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ e ∈ E → F e ∈ D
48 47 ex ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → e ∈ E → F e ∈ D
49 48 ralrimiv ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → ∀ e ∈ E F e ∈ D
50 uspgrupgr ⊢ H ∈ USHGraph → H ∈ UPGraph
51 50 ad3antlr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → H ∈ UPGraph
52 2 4 upgredg ⊢ H ∈ UPGraph ∧ d ∈ D → ∃ a ∈ W ∃ b ∈ W d = a b
53 51 52 sylan ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ d ∈ D → ∃ a ∈ W ∃ b ∈ W d = a b
54 f1ofo ⊢ F : V ⟶ 1-1 onto W → F : V ⟶ onto W
55 foelrn ⊢ F : V ⟶ onto W ∧ a ∈ W → ∃ m ∈ V a = F ⁡ m
56 55 ex ⊢ F : V ⟶ onto W → a ∈ W → ∃ m ∈ V a = F ⁡ m
57 foelrn ⊢ F : V ⟶ onto W ∧ b ∈ W → ∃ n ∈ V b = F ⁡ n
58 57 ex ⊢ F : V ⟶ onto W → b ∈ W → ∃ n ∈ V b = F ⁡ n
59 56 58 anim12d ⊢ F : V ⟶ onto W → a ∈ W ∧ b ∈ W → ∃ m ∈ V a = F ⁡ m ∧ ∃ n ∈ V b = F ⁡ n
60 54 59 syl ⊢ F : V ⟶ 1-1 onto W → a ∈ W ∧ b ∈ W → ∃ m ∈ V a = F ⁡ m ∧ ∃ n ∈ V b = F ⁡ n
61 60 adantl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W → a ∈ W ∧ b ∈ W → ∃ m ∈ V a = F ⁡ m ∧ ∃ n ∈ V b = F ⁡ n
62 61 adantr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → a ∈ W ∧ b ∈ W → ∃ m ∈ V a = F ⁡ m ∧ ∃ n ∈ V b = F ⁡ n
63 62 imp ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W → ∃ m ∈ V a = F ⁡ m ∧ ∃ n ∈ V b = F ⁡ n
64 preq12 ⊢ a = F ⁡ m ∧ b = F ⁡ n → a b = F ⁡ m F ⁡ n
65 64 eqeq2d ⊢ a = F ⁡ m ∧ b = F ⁡ n → d = a b ↔ d = F ⁡ m F ⁡ n
66 65 ancoms ⊢ b = F ⁡ n ∧ a = F ⁡ m → d = a b ↔ d = F ⁡ m F ⁡ n
67 66 adantl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W ∧ m ∈ V ∧ n ∈ V ∧ b = F ⁡ n ∧ a = F ⁡ m → d = a b ↔ d = F ⁡ m F ⁡ n
68 preq12 ⊢ x = m ∧ y = n → x y = m n
69 68 eleq1d ⊢ x = m ∧ y = n → x y ∈ E ↔ m n ∈ E
70 fveq2 ⊢ x = m → F ⁡ x = F ⁡ m
71 70 adantr ⊢ x = m ∧ y = n → F ⁡ x = F ⁡ m
72 fveq2 ⊢ y = n → F ⁡ y = F ⁡ n
73 72 adantl ⊢ x = m ∧ y = n → F ⁡ y = F ⁡ n
74 71 73 preq12d ⊢ x = m ∧ y = n → F ⁡ x F ⁡ y = F ⁡ m F ⁡ n
75 74 eleq1d ⊢ x = m ∧ y = n → F ⁡ x F ⁡ y ∈ D ↔ F ⁡ m F ⁡ n ∈ D
76 69 75 bibi12d ⊢ x = m ∧ y = n → x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ↔ m n ∈ E ↔ F ⁡ m F ⁡ n ∈ D
77 76 rspc2gv ⊢ m ∈ V ∧ n ∈ V → ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → m n ∈ E ↔ F ⁡ m F ⁡ n ∈ D
78 77 adantl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V → ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → m n ∈ E ↔ F ⁡ m F ⁡ n ∈ D
79 24 adantl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W → F Fn V
80 79 anim1i ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V → F Fn V ∧ m ∈ V ∧ n ∈ V
81 3anass ⊢ F Fn V ∧ m ∈ V ∧ n ∈ V ↔ F Fn V ∧ m ∈ V ∧ n ∈ V
82 80 81 sylibr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V → F Fn V ∧ m ∈ V ∧ n ∈ V
83 fnimapr ⊢ F Fn V ∧ m ∈ V ∧ n ∈ V → F m n = F ⁡ m F ⁡ n
84 82 83 syl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V → F m n = F ⁡ m F ⁡ n
85 84 eqcomd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V → F ⁡ m F ⁡ n = F m n
86 simpr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E ↔ F m n ∈ D → m n ∈ E ↔ F m n ∈ D
87 simpr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E → m n ∈ E
88 reueq ⊢ m n ∈ E ↔ ∃! e ∈ E e = m n
89 87 88 sylib ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E → ∃! e ∈ E e = m n
90 eqcom ⊢ m n = e ↔ e = m n
91 90 reubii ⊢ ∃! e ∈ E m n = e ↔ ∃! e ∈ E e = m n
92 89 91 sylibr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E → ∃! e ∈ E m n = e
93 f1of1 ⊢ F : V ⟶ 1-1 onto W → F : V ⟶ 1-1 W
94 93 adantl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W → F : V ⟶ 1-1 W
95 94 ad5ant12 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E ∧ e ∈ E → F : V ⟶ 1-1 W
96 prssi ⊢ m ∈ V ∧ n ∈ V → m n ⊆ V
97 96 ad3antlr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E ∧ e ∈ E → m n ⊆ V
98 uspgruhgr ⊢ G ∈ USHGraph → G ∈ UHGraph
99 98 adantr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → G ∈ UHGraph
100 99 ad5ant12 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E → G ∈ UHGraph
101 3 eleq2i ⊢ e ∈ E ↔ e ∈ Edg ⁡ G
102 101 biimpi ⊢ e ∈ E → e ∈ Edg ⁡ G
103 edguhgr ⊢ G ∈ UHGraph ∧ e ∈ Edg ⁡ G → e ∈ 𝒫 Vtx ⁡ G
104 1 pweqi ⊢ 𝒫 V = 𝒫 Vtx ⁡ G
105 103 104 eleqtrrdi ⊢ G ∈ UHGraph ∧ e ∈ Edg ⁡ G → e ∈ 𝒫 V
106 100 102 105 syl2an ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E ∧ e ∈ E → e ∈ 𝒫 V
107 106 elpwid ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E ∧ e ∈ E → e ⊆ V
108 f1imaeq ⊢ F : V ⟶ 1-1 W ∧ m n ⊆ V ∧ e ⊆ V → F m n = F e ↔ m n = e
109 95 97 107 108 syl12anc ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E ∧ e ∈ E → F m n = F e ↔ m n = e
110 109 reubidva ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E → ∃! e ∈ E F m n = F e ↔ ∃! e ∈ E m n = e
111 92 110 mpbird ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E → ∃! e ∈ E F m n = F e
112 111 ex ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V → m n ∈ E → ∃! e ∈ E F m n = F e
113 112 adantr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E ↔ F m n ∈ D → m n ∈ E → ∃! e ∈ E F m n = F e
114 86 113 sylbird ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V ∧ m n ∈ E ↔ F m n ∈ D → F m n ∈ D → ∃! e ∈ E F m n = F e
115 114 ex ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V → m n ∈ E ↔ F m n ∈ D → F m n ∈ D → ∃! e ∈ E F m n = F e
116 eleq1 ⊢ F ⁡ m F ⁡ n = F m n → F ⁡ m F ⁡ n ∈ D ↔ F m n ∈ D
117 116 bibi2d ⊢ F ⁡ m F ⁡ n = F m n → m n ∈ E ↔ F ⁡ m F ⁡ n ∈ D ↔ m n ∈ E ↔ F m n ∈ D
118 eqeq1 ⊢ F ⁡ m F ⁡ n = F m n → F ⁡ m F ⁡ n = F e ↔ F m n = F e
119 118 reubidv ⊢ F ⁡ m F ⁡ n = F m n → ∃! e ∈ E F ⁡ m F ⁡ n = F e ↔ ∃! e ∈ E F m n = F e
120 116 119 imbi12d ⊢ F ⁡ m F ⁡ n = F m n → F ⁡ m F ⁡ n ∈ D → ∃! e ∈ E F ⁡ m F ⁡ n = F e ↔ F m n ∈ D → ∃! e ∈ E F m n = F e
121 117 120 imbi12d ⊢ F ⁡ m F ⁡ n = F m n → m n ∈ E ↔ F ⁡ m F ⁡ n ∈ D → F ⁡ m F ⁡ n ∈ D → ∃! e ∈ E F ⁡ m F ⁡ n = F e ↔ m n ∈ E ↔ F m n ∈ D → F m n ∈ D → ∃! e ∈ E F m n = F e
122 115 121 syl5ibrcom ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V → F ⁡ m F ⁡ n = F m n → m n ∈ E ↔ F ⁡ m F ⁡ n ∈ D → F ⁡ m F ⁡ n ∈ D → ∃! e ∈ E F ⁡ m F ⁡ n = F e
123 85 122 mpd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V → m n ∈ E ↔ F ⁡ m F ⁡ n ∈ D → F ⁡ m F ⁡ n ∈ D → ∃! e ∈ E F ⁡ m F ⁡ n = F e
124 78 123 syld ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ m ∈ V ∧ n ∈ V → ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → F ⁡ m F ⁡ n ∈ D → ∃! e ∈ E F ⁡ m F ⁡ n = F e
125 124 impancom ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → m ∈ V ∧ n ∈ V → F ⁡ m F ⁡ n ∈ D → ∃! e ∈ E F ⁡ m F ⁡ n = F e
126 125 adantr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W → m ∈ V ∧ n ∈ V → F ⁡ m F ⁡ n ∈ D → ∃! e ∈ E F ⁡ m F ⁡ n = F e
127 126 impl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W ∧ m ∈ V ∧ n ∈ V → F ⁡ m F ⁡ n ∈ D → ∃! e ∈ E F ⁡ m F ⁡ n = F e
128 eleq1 ⊢ d = F ⁡ m F ⁡ n → d ∈ D ↔ F ⁡ m F ⁡ n ∈ D
129 eqeq1 ⊢ d = F ⁡ m F ⁡ n → d = F e ↔ F ⁡ m F ⁡ n = F e
130 129 reubidv ⊢ d = F ⁡ m F ⁡ n → ∃! e ∈ E d = F e ↔ ∃! e ∈ E F ⁡ m F ⁡ n = F e
131 128 130 imbi12d ⊢ d = F ⁡ m F ⁡ n → d ∈ D → ∃! e ∈ E d = F e ↔ F ⁡ m F ⁡ n ∈ D → ∃! e ∈ E F ⁡ m F ⁡ n = F e
132 127 131 syl5ibrcom ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W ∧ m ∈ V ∧ n ∈ V → d = F ⁡ m F ⁡ n → d ∈ D → ∃! e ∈ E d = F e
133 132 adantr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W ∧ m ∈ V ∧ n ∈ V ∧ b = F ⁡ n ∧ a = F ⁡ m → d = F ⁡ m F ⁡ n → d ∈ D → ∃! e ∈ E d = F e
134 67 133 sylbid ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W ∧ m ∈ V ∧ n ∈ V ∧ b = F ⁡ n ∧ a = F ⁡ m → d = a b → d ∈ D → ∃! e ∈ E d = F e
135 134 exp32 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W ∧ m ∈ V ∧ n ∈ V → b = F ⁡ n → a = F ⁡ m → d = a b → d ∈ D → ∃! e ∈ E d = F e
136 135 rexlimdva ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W ∧ m ∈ V → ∃ n ∈ V b = F ⁡ n → a = F ⁡ m → d = a b → d ∈ D → ∃! e ∈ E d = F e
137 136 com23 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W ∧ m ∈ V → a = F ⁡ m → ∃ n ∈ V b = F ⁡ n → d = a b → d ∈ D → ∃! e ∈ E d = F e
138 137 rexlimdva ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W → ∃ m ∈ V a = F ⁡ m → ∃ n ∈ V b = F ⁡ n → d = a b → d ∈ D → ∃! e ∈ E d = F e
139 138 impd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W → ∃ m ∈ V a = F ⁡ m ∧ ∃ n ∈ V b = F ⁡ n → d = a b → d ∈ D → ∃! e ∈ E d = F e
140 63 139 mpd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W → d = a b → d ∈ D → ∃! e ∈ E d = F e
141 140 com23 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ a ∈ W ∧ b ∈ W → d ∈ D → d = a b → ∃! e ∈ E d = F e
142 141 impancom ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ d ∈ D → a ∈ W ∧ b ∈ W → d = a b → ∃! e ∈ E d = F e
143 142 rexlimdvv ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ d ∈ D → ∃ a ∈ W ∃ b ∈ W d = a b → ∃! e ∈ E d = F e
144 53 143 mpd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D ∧ d ∈ D → ∃! e ∈ E d = F e
145 144 ralrimiva ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → ∀ d ∈ D ∃! e ∈ E d = F e
146 eqid ⊢ e ∈ E ⟼ F e = e ∈ E ⟼ F e
147 146 f1ompt ⊢ e ∈ E ⟼ F e : E ⟶ 1-1 onto D ↔ ∀ e ∈ E F e ∈ D ∧ ∀ d ∈ D ∃! e ∈ E d = F e
148 49 145 147 sylanbrc ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F : V ⟶ 1-1 onto W ∧ ∀ x ∈ V ∀ y ∈ V x y ∈ E ↔ F ⁡ x F ⁡ y ∈ D → e ∈ E ⟼ F e : E ⟶ 1-1 onto D