Step | Hyp | Ref
| Expression |
1 | | eqidd 2738 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑓 = 𝑓) |
2 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (Vtx‘𝑥) = (Vtx‘𝐴)) |
3 | 2 | adantr 484 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (Vtx‘𝑥) = (Vtx‘𝐴)) |
4 | | isomgr.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐴) |
5 | 3, 4 | eqtr4di 2796 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (Vtx‘𝑥) = 𝑉) |
6 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (Vtx‘𝑦) = (Vtx‘𝐵)) |
7 | 6 | adantl 485 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (Vtx‘𝑦) = (Vtx‘𝐵)) |
8 | | isomgr.w |
. . . . . 6
⊢ 𝑊 = (Vtx‘𝐵) |
9 | 7, 8 | eqtr4di 2796 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (Vtx‘𝑦) = 𝑊) |
10 | 1, 5, 9 | f1oeq123d 6655 |
. . . 4
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ↔ 𝑓:𝑉–1-1-onto→𝑊)) |
11 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑔 = 𝑔) |
12 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (iEdg‘𝑥) = (iEdg‘𝐴)) |
13 | 12 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (iEdg‘𝑥) = (iEdg‘𝐴)) |
14 | | isomgr.i |
. . . . . . . . 9
⊢ 𝐼 = (iEdg‘𝐴) |
15 | 13, 14 | eqtr4di 2796 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (iEdg‘𝑥) = 𝐼) |
16 | 15 | dmeqd 5774 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → dom (iEdg‘𝑥) = dom 𝐼) |
17 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → (iEdg‘𝑦) = (iEdg‘𝐵)) |
18 | 17 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (iEdg‘𝑦) = (iEdg‘𝐵)) |
19 | | isomgr.j |
. . . . . . . . 9
⊢ 𝐽 = (iEdg‘𝐵) |
20 | 18, 19 | eqtr4di 2796 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (iEdg‘𝑦) = 𝐽) |
21 | 20 | dmeqd 5774 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → dom (iEdg‘𝑦) = dom 𝐽) |
22 | 11, 16, 21 | f1oeq123d 6655 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑔:dom (iEdg‘𝑥)–1-1-onto→dom
(iEdg‘𝑦) ↔ 𝑔:dom 𝐼–1-1-onto→dom
𝐽)) |
23 | 15 | fveq1d 6719 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ((iEdg‘𝑥)‘𝑖) = (𝐼‘𝑖)) |
24 | 23 | imaeq2d 5929 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑓 “ ((iEdg‘𝑥)‘𝑖)) = (𝑓 “ (𝐼‘𝑖))) |
25 | 20 | fveq1d 6719 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ((iEdg‘𝑦)‘(𝑔‘𝑖)) = (𝐽‘(𝑔‘𝑖))) |
26 | 24, 25 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ((𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)) ↔ (𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))) |
27 | 16, 26 | raleqbidv 3313 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)) ↔ ∀𝑖 ∈ dom 𝐼(𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))) |
28 | 22, 27 | anbi12d 634 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ((𝑔:dom (iEdg‘𝑥)–1-1-onto→dom
(iEdg‘𝑦) ∧
∀𝑖 ∈ dom
(iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖))) ↔ (𝑔:dom 𝐼–1-1-onto→dom
𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖))))) |
29 | 28 | exbidv 1929 |
. . . 4
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom
(iEdg‘𝑦) ∧
∀𝑖 ∈ dom
(iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖))) ↔ ∃𝑔(𝑔:dom 𝐼–1-1-onto→dom
𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖))))) |
30 | 10, 29 | anbi12d 634 |
. . 3
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ((𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom
(iEdg‘𝑦) ∧
∀𝑖 ∈ dom
(iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))) ↔ (𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:dom 𝐼–1-1-onto→dom
𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))) |
31 | 30 | exbidv 1929 |
. 2
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑓(𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom
(iEdg‘𝑦) ∧
∀𝑖 ∈ dom
(iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))) ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:dom 𝐼–1-1-onto→dom
𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))) |
32 | | df-isomgr 44949 |
. 2
⊢ IsomGr =
{〈𝑥, 𝑦〉 ∣ ∃𝑓(𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom
(iEdg‘𝑦) ∧
∀𝑖 ∈ dom
(iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖))))} |
33 | 31, 32 | brabga 5415 |
1
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴 IsomGr 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:dom 𝐼–1-1-onto→dom
𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))) |