Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . 3
⊢
(Vtx‘𝐴) =
(Vtx‘𝐴) |
2 | | eqid 2738 |
. . 3
⊢
(Vtx‘𝐵) =
(Vtx‘𝐵) |
3 | | eqid 2738 |
. . 3
⊢
(iEdg‘𝐴) =
(iEdg‘𝐴) |
4 | | eqid 2738 |
. . 3
⊢
(iEdg‘𝐵) =
(iEdg‘𝐵) |
5 | 1, 2, 3, 4 | isomgr 45275 |
. 2
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) → (𝐴 IsomGr 𝐵 ↔ ∃𝑓(𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)))))) |
6 | | vex 3436 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
7 | 6 | cnvex 7772 |
. . . . . . 7
⊢ ◡𝑓 ∈ V |
8 | 7 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))))) → ◡𝑓 ∈ V) |
9 | | f1ocnv 6728 |
. . . . . . . . 9
⊢ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → ◡𝑓:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴)) |
10 | 9 | adantr 481 |
. . . . . . . 8
⊢ ((𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)))) → ◡𝑓:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴)) |
11 | 10 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))))) → ◡𝑓:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴)) |
12 | | vex 3436 |
. . . . . . . . . . . . . 14
⊢ 𝑔 ∈ V |
13 | 12 | cnvex 7772 |
. . . . . . . . . . . . 13
⊢ ◡𝑔 ∈ V |
14 | 13 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → ◡𝑔 ∈ V) |
15 | | f1ocnv 6728 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) → ◡𝑔:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴)) |
16 | 15 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) → ◡𝑔:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴)) |
17 | 16 | 3ad2ant2 1133 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → ◡𝑔:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴)) |
18 | | f1ocnvdm 7157 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (◡𝑔‘𝑗) ∈ dom (iEdg‘𝐴)) |
19 | 18 | 3ad2antl2 1185 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (◡𝑔‘𝑗) ∈ dom (iEdg‘𝐴)) |
20 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 = (◡𝑔‘𝑗) → ((iEdg‘𝐴)‘𝑖) = ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) |
21 | 20 | imaeq2d 5969 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = (◡𝑔‘𝑗) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗)))) |
22 | | 2fveq3 6779 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = (◡𝑔‘𝑗) → ((iEdg‘𝐵)‘(𝑔‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘(◡𝑔‘𝑗)))) |
23 | 21, 22 | eqeq12d 2754 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 = (◡𝑔‘𝑗) → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) = ((iEdg‘𝐵)‘(𝑔‘(◡𝑔‘𝑗))))) |
24 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐴 ∈
UHGraph ∧ 𝐵 ∈
𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) ∧ 𝑖 = (◡𝑔‘𝑗)) → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) = ((iEdg‘𝐵)‘(𝑔‘(◡𝑔‘𝑗))))) |
25 | 19, 24 | rspcdv 3553 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)) → (𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) = ((iEdg‘𝐵)‘(𝑔‘(◡𝑔‘𝑗))))) |
26 | | f1ocnvfv2 7149 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (𝑔‘(◡𝑔‘𝑗)) = 𝑗) |
27 | 26 | 3ad2antl2 1185 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (𝑔‘(◡𝑔‘𝑗)) = 𝑗) |
28 | 27 | fveq2d 6778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → ((iEdg‘𝐵)‘(𝑔‘(◡𝑔‘𝑗))) = ((iEdg‘𝐵)‘𝑗)) |
29 | 28 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → ((𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) = ((iEdg‘𝐵)‘(𝑔‘(◡𝑔‘𝑗))) ↔ (𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) = ((iEdg‘𝐵)‘𝑗))) |
30 | | f1of1 6715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → 𝑓:(Vtx‘𝐴)–1-1→(Vtx‘𝐵)) |
31 | 30 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → 𝑓:(Vtx‘𝐴)–1-1→(Vtx‘𝐵)) |
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → 𝑓:(Vtx‘𝐴)–1-1→(Vtx‘𝐵)) |
33 | | simpl1l 1223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → 𝐴 ∈ UHGraph) |
34 | 1, 3 | uhgrss 27434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐴 ∈ UHGraph ∧ (◡𝑔‘𝑗) ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) ⊆ (Vtx‘𝐴)) |
35 | 33, 19, 34 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) ⊆ (Vtx‘𝐴)) |
36 | 32, 35 | jca 512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (𝑓:(Vtx‘𝐴)–1-1→(Vtx‘𝐵) ∧ ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) ⊆ (Vtx‘𝐴))) |
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐴 ∈
UHGraph ∧ 𝐵 ∈
𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) ∧ (𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) = ((iEdg‘𝐵)‘𝑗)) → (𝑓:(Vtx‘𝐴)–1-1→(Vtx‘𝐵) ∧ ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) ⊆ (Vtx‘𝐴))) |
38 | | f1imacnv 6732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓:(Vtx‘𝐴)–1-1→(Vtx‘𝐵) ∧ ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) ⊆ (Vtx‘𝐴)) → (◡𝑓 “ (𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗)))) = ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐴 ∈
UHGraph ∧ 𝐵 ∈
𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) ∧ (𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) = ((iEdg‘𝐵)‘𝑗)) → (◡𝑓 “ (𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗)))) = ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) |
40 | | imaeq2 5965 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) = ((iEdg‘𝐵)‘𝑗) → (◡𝑓 “ (𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗)))) = (◡𝑓 “ ((iEdg‘𝐵)‘𝑗))) |
41 | 40 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐴 ∈
UHGraph ∧ 𝐵 ∈
𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) ∧ (𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) = ((iEdg‘𝐵)‘𝑗)) → (◡𝑓 “ (𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗)))) = (◡𝑓 “ ((iEdg‘𝐵)‘𝑗))) |
42 | 39, 41 | eqtr3d 2780 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐴 ∈
UHGraph ∧ 𝐵 ∈
𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) ∧ (𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) = ((iEdg‘𝐵)‘𝑗)) → ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) = (◡𝑓 “ ((iEdg‘𝐵)‘𝑗))) |
43 | 42 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → ((𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) = ((iEdg‘𝐵)‘𝑗) → ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) = (◡𝑓 “ ((iEdg‘𝐵)‘𝑗)))) |
44 | 29, 43 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → ((𝑓 “ ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) = ((iEdg‘𝐵)‘(𝑔‘(◡𝑔‘𝑗))) → ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) = (◡𝑓 “ ((iEdg‘𝐵)‘𝑗)))) |
45 | 25, 44 | syld 47 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)) → ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) = (◡𝑓 “ ((iEdg‘𝐵)‘𝑗)))) |
46 | 45 | ex 413 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → (𝑗 ∈ dom (iEdg‘𝐵) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)) → ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) = (◡𝑓 “ ((iEdg‘𝐵)‘𝑗))))) |
47 | 46 | com23 86 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)) → (𝑗 ∈ dom (iEdg‘𝐵) → ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) = (◡𝑓 “ ((iEdg‘𝐵)‘𝑗))))) |
48 | 47 | 3exp 1118 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) → (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) →
(𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)) → (𝑗 ∈ dom (iEdg‘𝐵) → ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) = (◡𝑓 “ ((iEdg‘𝐵)‘𝑗))))))) |
49 | 48 | com34 91 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) → (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) →
(∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)) → (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → (𝑗 ∈ dom (iEdg‘𝐵) → ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) = (◡𝑓 “ ((iEdg‘𝐵)‘𝑗))))))) |
50 | 49 | impd 411 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) → ((𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) → (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → (𝑗 ∈ dom (iEdg‘𝐵) → ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) = (◡𝑓 “ ((iEdg‘𝐵)‘𝑗)))))) |
51 | 50 | 3imp1 1346 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → ((iEdg‘𝐴)‘(◡𝑔‘𝑗)) = (◡𝑓 “ ((iEdg‘𝐵)‘𝑗))) |
52 | 51 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) |
53 | 52 | ralrimiva 3103 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → ∀𝑗 ∈ dom (iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) |
54 | 17, 53 | jca 512 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → (◡𝑔:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(◡𝑔‘𝑗)))) |
55 | | f1oeq1 6704 |
. . . . . . . . . . . . 13
⊢ (ℎ = ◡𝑔 → (ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ↔ ◡𝑔:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴))) |
56 | | fveq1 6773 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = ◡𝑔 → (ℎ‘𝑗) = (◡𝑔‘𝑗)) |
57 | 56 | fveq2d 6778 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = ◡𝑔 → ((iEdg‘𝐴)‘(ℎ‘𝑗)) = ((iEdg‘𝐴)‘(◡𝑔‘𝑗))) |
58 | 57 | eqeq2d 2749 |
. . . . . . . . . . . . . 14
⊢ (ℎ = ◡𝑔 → ((◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)) ↔ (◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(◡𝑔‘𝑗)))) |
59 | 58 | ralbidv 3112 |
. . . . . . . . . . . . 13
⊢ (ℎ = ◡𝑔 → (∀𝑗 ∈ dom (iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)) ↔ ∀𝑗 ∈ dom (iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(◡𝑔‘𝑗)))) |
60 | 55, 59 | anbi12d 631 |
. . . . . . . . . . . 12
⊢ (ℎ = ◡𝑔 → ((ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗))) ↔ (◡𝑔:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(◡𝑔‘𝑗))))) |
61 | 14, 54, 60 | spcedv 3537 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → ∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)))) |
62 | 61 | 3exp 1118 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) → ((𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) → (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → ∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)))))) |
63 | 62 | exlimdv 1936 |
. . . . . . . . 9
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) → (∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) → (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → ∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)))))) |
64 | 63 | com23 86 |
. . . . . . . 8
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) → (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → (∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) → ∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)))))) |
65 | 64 | imp32 419 |
. . . . . . 7
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))))) → ∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)))) |
66 | 11, 65 | jca 512 |
. . . . . 6
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))))) → (◡𝑓:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗))))) |
67 | | f1oeq1 6704 |
. . . . . . 7
⊢ (𝑒 = ◡𝑓 → (𝑒:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ↔ ◡𝑓:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴))) |
68 | | imaeq1 5964 |
. . . . . . . . . . 11
⊢ (𝑒 = ◡𝑓 → (𝑒 “ ((iEdg‘𝐵)‘𝑗)) = (◡𝑓 “ ((iEdg‘𝐵)‘𝑗))) |
69 | 68 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (𝑒 = ◡𝑓 → ((𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)) ↔ (◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)))) |
70 | 69 | ralbidv 3112 |
. . . . . . . . 9
⊢ (𝑒 = ◡𝑓 → (∀𝑗 ∈ dom (iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)) ↔ ∀𝑗 ∈ dom (iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)))) |
71 | 70 | anbi2d 629 |
. . . . . . . 8
⊢ (𝑒 = ◡𝑓 → ((ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗))) ↔ (ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗))))) |
72 | 71 | exbidv 1924 |
. . . . . . 7
⊢ (𝑒 = ◡𝑓 → (∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗))) ↔ ∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗))))) |
73 | 67, 72 | anbi12d 631 |
. . . . . 6
⊢ (𝑒 = ◡𝑓 → ((𝑒:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)))) ↔ (◡𝑓:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(◡𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)))))) |
74 | 8, 66, 73 | spcedv 3537 |
. . . . 5
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))))) → ∃𝑒(𝑒:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗))))) |
75 | 2, 1, 4, 3 | isomgr 45275 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ UHGraph) → (𝐵 IsomGr 𝐴 ↔ ∃𝑒(𝑒:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)))))) |
76 | 75 | ancoms 459 |
. . . . . 6
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) → (𝐵 IsomGr 𝐴 ↔ ∃𝑒(𝑒:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)))))) |
77 | 76 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))))) → (𝐵 IsomGr 𝐴 ↔ ∃𝑒(𝑒:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃ℎ(ℎ:dom (iEdg‘𝐵)–1-1-onto→dom
(iEdg‘𝐴) ∧
∀𝑗 ∈ dom
(iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(ℎ‘𝑗)))))) |
78 | 74, 77 | mpbird 256 |
. . . 4
⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))))) → 𝐵 IsomGr 𝐴) |
79 | 78 | ex 413 |
. . 3
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) → ((𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)))) → 𝐵 IsomGr 𝐴)) |
80 | 79 | exlimdv 1936 |
. 2
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) → (∃𝑓(𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom
(iEdg‘𝐵) ∧
∀𝑖 ∈ dom
(iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)))) → 𝐵 IsomGr 𝐴)) |
81 | 5, 80 | sylbid 239 |
1
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) → (𝐴 IsomGr 𝐵 → 𝐵 IsomGr 𝐴)) |