| Step | Hyp | Ref
| Expression |
| 1 | | isusgrim.v |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | | isusgrim.w |
. . 3
⊢ 𝑊 = (Vtx‘𝐻) |
| 3 | | eqid 2737 |
. . 3
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 4 | | eqid 2737 |
. . 3
⊢
(iEdg‘𝐻) =
(iEdg‘𝐻) |
| 5 | 1, 2, 3, 4 | isgrim 47868 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))) |
| 6 | | isusgrim.e |
. . . . . . . . . . . . . . 15
⊢ 𝐸 = (Edg‘𝐺) |
| 7 | 6 | eleq2i 2833 |
. . . . . . . . . . . . . 14
⊢ (𝑒 ∈ 𝐸 ↔ 𝑒 ∈ (Edg‘𝐺)) |
| 8 | | uspgruhgr 29201 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈
UHGraph) |
| 9 | 3 | uhgredgiedgb 29143 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ UHGraph → (𝑒 ∈ (Edg‘𝐺) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘))) |
| 10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ USPGraph → (𝑒 ∈ (Edg‘𝐺) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘))) |
| 11 | 7, 10 | bitrid 283 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USPGraph → (𝑒 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘))) |
| 12 | 11 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → (𝑒 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘))) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (𝑒 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘))) |
| 14 | 13 | biimpa 476 |
. . . . . . . . . 10
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑒 ∈ 𝐸) → ∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘)) |
| 15 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑘 → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘𝑘))) |
| 16 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = 𝑘 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑘)) |
| 17 | 16 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑘 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))) |
| 18 | 15, 17 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑘 → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))) |
| 19 | 18 | rspcv 3618 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))) |
| 20 | 19 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))) |
| 21 | | uspgruhgr 29201 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐻 ∈ USPGraph → 𝐻 ∈
UHGraph) |
| 22 | 4 | uhgrfun 29083 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐻 ∈ UHGraph → Fun
(iEdg‘𝐻)) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐻 ∈ USPGraph → Fun
(iEdg‘𝐻)) |
| 24 | 23 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → Fun (iEdg‘𝐻)) |
| 25 | 24 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → Fun (iEdg‘𝐻)) |
| 26 | | f1of 6848 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) → 𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻)) |
| 27 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) →
𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻)) |
| 28 | 27 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝑗‘𝑘) ∈ dom (iEdg‘𝐻)) |
| 29 | 4 | iedgedg 29067 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Fun
(iEdg‘𝐻) ∧ (𝑗‘𝑘) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ (Edg‘𝐻)) |
| 30 | 25, 28, 29 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ (Edg‘𝐻)) |
| 31 | | isusgrim.d |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐷 = (Edg‘𝐻) |
| 32 | 31 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐷 ↔ ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ (Edg‘𝐻)) |
| 33 | 30, 32 | sylibr 234 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐷) |
| 34 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → (((iEdg‘𝐻)‘(𝑗‘𝑘)) ∈ 𝐷 ↔ (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)) |
| 35 | 33, 34 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑗‘𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)) |
| 36 | 20, 35 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)) |
| 37 | 36 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) →
(𝑘 ∈ dom
(iEdg‘𝐺) →
(∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷))) |
| 38 | 37 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) →
(∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝑘 ∈ dom (iEdg‘𝐺) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷))) |
| 39 | 38 | impr 454 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (𝑘 ∈ dom (iEdg‘𝐺) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑒 ∈ 𝐸) → (𝑘 ∈ dom (iEdg‘𝐺) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)) |
| 41 | 40 | imp 406 |
. . . . . . . . . . . 12
⊢
((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑒 ∈ 𝐸) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷) |
| 42 | | imaeq2 6074 |
. . . . . . . . . . . . 13
⊢ (𝑒 = ((iEdg‘𝐺)‘𝑘) → (𝐹 “ 𝑒) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))) |
| 43 | 42 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑒 = ((iEdg‘𝐺)‘𝑘) → ((𝐹 “ 𝑒) ∈ 𝐷 ↔ (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)) |
| 44 | 41, 43 | syl5ibrcom 247 |
. . . . . . . . . . 11
⊢
((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑒 ∈ 𝐸) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝑒 = ((iEdg‘𝐺)‘𝑘) → (𝐹 “ 𝑒) ∈ 𝐷)) |
| 45 | 44 | rexlimdva 3155 |
. . . . . . . . . 10
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑒 ∈ 𝐸) → (∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘) → (𝐹 “ 𝑒) ∈ 𝐷)) |
| 46 | 14, 45 | mpd 15 |
. . . . . . . . 9
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑒 ∈ 𝐸) → (𝐹 “ 𝑒) ∈ 𝐷) |
| 47 | 46 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ∀𝑒 ∈ 𝐸 (𝐹 “ 𝑒) ∈ 𝐷) |
| 48 | 31 | eleq2i 2833 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ 𝐷 ↔ 𝑑 ∈ (Edg‘𝐻)) |
| 49 | 4 | uhgredgiedgb 29143 |
. . . . . . . . . . . . . 14
⊢ (𝐻 ∈ UHGraph → (𝑑 ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝑑 = ((iEdg‘𝐻)‘𝑘))) |
| 50 | 21, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐻 ∈ USPGraph → (𝑑 ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝑑 = ((iEdg‘𝐻)‘𝑘))) |
| 51 | 48, 50 | bitrid 283 |
. . . . . . . . . . . 12
⊢ (𝐻 ∈ USPGraph → (𝑑 ∈ 𝐷 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝑑 = ((iEdg‘𝐻)‘𝑘))) |
| 52 | 51 | 3ad2ant2 1135 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → (𝑑 ∈ 𝐷 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝑑 = ((iEdg‘𝐻)‘𝑘))) |
| 53 | 52 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (𝑑 ∈ 𝐷 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝑑 = ((iEdg‘𝐻)‘𝑘))) |
| 54 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) |
| 55 | | f1ocnvdm 7305 |
. . . . . . . . . . . . 13
⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) |
| 56 | 54, 55 | sylan 580 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) |
| 57 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = (◡𝑗‘𝑘) → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘(◡𝑗‘𝑘)))) |
| 58 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = (◡𝑗‘𝑘) → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) |
| 59 | 58 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = (◡𝑗‘𝑘) → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) |
| 60 | 57, 59 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (◡𝑗‘𝑘) → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘(◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) |
| 61 | 60 | rspccv 3619 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑖 ∈
dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐻)‘(𝑗‘(◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) |
| 62 | 61 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐻)‘(𝑗‘(◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) |
| 63 | 62 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ((◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐻)‘(𝑗‘(◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) |
| 64 | 63 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐻)‘(𝑗‘(◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) |
| 65 | | f1ocnvfv2 7297 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑗‘(◡𝑗‘𝑘)) = 𝑘) |
| 66 | 54, 65 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑗‘(◡𝑗‘𝑘)) = 𝑘) |
| 67 | 66 | fveqeq2d 6914 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (((iEdg‘𝐻)‘(𝑗‘(◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) ↔ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) |
| 68 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . 17
⊢
(((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) → (𝑑 = ((iEdg‘𝐻)‘𝑘) ↔ 𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) |
| 69 | 68 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) → (𝑑 = ((iEdg‘𝐻)‘𝑘) ↔ 𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) |
| 70 | | simpll1 1213 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → 𝐺 ∈ USPGraph) |
| 71 | 6, 3 | uspgriedgedg 29193 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺 ∈ USPGraph ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ∃!𝑒 ∈ 𝐸 𝑒 = ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) |
| 72 | 70, 56, 71 | syl2an2r 685 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃!𝑒 ∈ 𝐸 𝑒 = ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) |
| 73 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((iEdg‘𝐺)‘(◡𝑗‘𝑘)) = 𝑒 ↔ 𝑒 = ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) |
| 74 | 73 | reubii 3389 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃!𝑒 ∈
𝐸 ((iEdg‘𝐺)‘(◡𝑗‘𝑘)) = 𝑒 ↔ ∃!𝑒 ∈ 𝐸 𝑒 = ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) |
| 75 | 72, 74 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃!𝑒 ∈ 𝐸 ((iEdg‘𝐺)‘(◡𝑗‘𝑘)) = 𝑒) |
| 76 | | f1of1 6847 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–1-1→𝑊) |
| 77 | 76 | ad4antlr 733 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒 ∈ 𝐸) → 𝐹:𝑉–1-1→𝑊) |
| 78 | | uspgrupgr 29195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈
UPGraph) |
| 79 | 78 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → 𝐺 ∈ UPGraph) |
| 80 | 79 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → 𝐺 ∈ UPGraph) |
| 81 | 80, 56 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝐺 ∈ UPGraph ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺))) |
| 82 | 81 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒 ∈ 𝐸) → (𝐺 ∈ UPGraph ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺))) |
| 83 | 1, 3 | upgrss 29105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ UPGraph ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(◡𝑗‘𝑘)) ⊆ 𝑉) |
| 84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒 ∈ 𝐸) → ((iEdg‘𝐺)‘(◡𝑗‘𝑘)) ⊆ 𝑉) |
| 85 | 7 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑒 ∈ 𝐸 → 𝑒 ∈ (Edg‘𝐺)) |
| 86 | | edgupgr 29151 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺 ∈ UPGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → (𝑒 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝑒 ≠ ∅ ∧ (♯‘𝑒) ≤ 2)) |
| 87 | 80, 85, 86 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒 ∈ 𝐸) → (𝑒 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝑒 ≠ ∅ ∧ (♯‘𝑒) ≤ 2)) |
| 88 | 87 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒 ∈ 𝐸) → 𝑒 ∈ 𝒫 (Vtx‘𝐺)) |
| 89 | 88 | elpwid 4609 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒 ∈ 𝐸) → 𝑒 ⊆ (Vtx‘𝐺)) |
| 90 | 89, 1 | sseqtrrdi 4025 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒 ∈ 𝐸) → 𝑒 ⊆ 𝑉) |
| 91 | | f1imaeq 7285 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹:𝑉–1-1→𝑊 ∧ (((iEdg‘𝐺)‘(◡𝑗‘𝑘)) ⊆ 𝑉 ∧ 𝑒 ⊆ 𝑉)) → ((𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) = (𝐹 “ 𝑒) ↔ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)) = 𝑒)) |
| 92 | 77, 84, 90, 91 | syl12anc 837 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒 ∈ 𝐸) → ((𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) = (𝐹 “ 𝑒) ↔ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)) = 𝑒)) |
| 93 | 92 | reubidva 3396 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (∃!𝑒 ∈ 𝐸 (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) = (𝐹 “ 𝑒) ↔ ∃!𝑒 ∈ 𝐸 ((iEdg‘𝐺)‘(◡𝑗‘𝑘)) = 𝑒)) |
| 94 | 75, 93 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃!𝑒 ∈ 𝐸 (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) = (𝐹 “ 𝑒)) |
| 95 | 94 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) ∧ 𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) → ∃!𝑒 ∈ 𝐸 (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) = (𝐹 “ 𝑒)) |
| 96 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) → (𝑑 = (𝐹 “ 𝑒) ↔ (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) = (𝐹 “ 𝑒))) |
| 97 | 96 | reubidv 3398 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) → (∃!𝑒 ∈ 𝐸 𝑑 = (𝐹 “ 𝑒) ↔ ∃!𝑒 ∈ 𝐸 (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) = (𝐹 “ 𝑒))) |
| 98 | 97 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) ∧ 𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) → (∃!𝑒 ∈ 𝐸 𝑑 = (𝐹 “ 𝑒) ↔ ∃!𝑒 ∈ 𝐸 (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) = (𝐹 “ 𝑒))) |
| 99 | 95, 98 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) ∧ 𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) → ∃!𝑒 ∈ 𝐸 𝑑 = (𝐹 “ 𝑒)) |
| 100 | 99 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) → (𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) → ∃!𝑒 ∈ 𝐸 𝑑 = (𝐹 “ 𝑒))) |
| 101 | 69, 100 | sylbid 240 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) → (𝑑 = ((iEdg‘𝐻)‘𝑘) → ∃!𝑒 ∈ 𝐸 𝑑 = (𝐹 “ 𝑒))) |
| 102 | 101 | ex 412 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) → (𝑑 = ((iEdg‘𝐻)‘𝑘) → ∃!𝑒 ∈ 𝐸 𝑑 = (𝐹 “ 𝑒)))) |
| 103 | 67, 102 | sylbid 240 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (((iEdg‘𝐻)‘(𝑗‘(◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) → (𝑑 = ((iEdg‘𝐻)‘𝑘) → ∃!𝑒 ∈ 𝐸 𝑑 = (𝐹 “ 𝑒)))) |
| 104 | 64, 103 | syld 47 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → (𝑑 = ((iEdg‘𝐻)‘𝑘) → ∃!𝑒 ∈ 𝐸 𝑑 = (𝐹 “ 𝑒)))) |
| 105 | 56, 104 | mpd 15 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈
USPGraph ∧ 𝐻 ∈
USPGraph ∧ 𝐹 ∈
𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑑 = ((iEdg‘𝐻)‘𝑘) → ∃!𝑒 ∈ 𝐸 𝑑 = (𝐹 “ 𝑒))) |
| 106 | 105 | rexlimdva 3155 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (∃𝑘 ∈ dom (iEdg‘𝐻)𝑑 = ((iEdg‘𝐻)‘𝑘) → ∃!𝑒 ∈ 𝐸 𝑑 = (𝐹 “ 𝑒))) |
| 107 | 53, 106 | sylbid 240 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (𝑑 ∈ 𝐷 → ∃!𝑒 ∈ 𝐸 𝑑 = (𝐹 “ 𝑒))) |
| 108 | 107 | ralrimiv 3145 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ∀𝑑 ∈ 𝐷 ∃!𝑒 ∈ 𝐸 𝑑 = (𝐹 “ 𝑒)) |
| 109 | | imaeq2 6074 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑒 → (𝐹 “ 𝑥) = (𝐹 “ 𝑒)) |
| 110 | 109 | cbvmptv 5255 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)) = (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) |
| 111 | 110 | f1ompt 7131 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)):𝐸–1-1-onto→𝐷 ↔ (∀𝑒 ∈ 𝐸 (𝐹 “ 𝑒) ∈ 𝐷 ∧ ∀𝑑 ∈ 𝐷 ∃!𝑒 ∈ 𝐸 𝑑 = (𝐹 “ 𝑒))) |
| 112 | 47, 108, 111 | sylanbrc 583 |
. . . . . . 7
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)):𝐸–1-1-onto→𝐷) |
| 113 | 112 | ex 412 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)):𝐸–1-1-onto→𝐷)) |
| 114 | 113 | exlimdv 1933 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)):𝐸–1-1-onto→𝐷)) |
| 115 | | fvex 6919 |
. . . . . . . . . 10
⊢
(iEdg‘𝐺)
∈ V |
| 116 | 115 | dmex 7931 |
. . . . . . . . 9
⊢ dom
(iEdg‘𝐺) ∈
V |
| 117 | 116 | mptex 7243 |
. . . . . . . 8
⊢ (𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒)))) ∈ V |
| 118 | 117 | a1i 11 |
. . . . . . 7
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)):𝐸–1-1-onto→𝐷) → (𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒)))) ∈ V) |
| 119 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒)))) = (𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒)))) |
| 120 | 1, 2, 6, 31, 3, 4,
110, 119 | isuspgrim0lem 47871 |
. . . . . . 7
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)):𝐸–1-1-onto→𝐷) → ((𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒)))):dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘((𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒))))‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) |
| 121 | | f1oeq1 6836 |
. . . . . . . 8
⊢ (𝑗 = (𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒)))) → (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ↔
(𝑒 ∈ dom
(iEdg‘𝐺) ↦
(◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒)))):dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻))) |
| 122 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒)))) → (𝑗‘𝑖) = ((𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒))))‘𝑖)) |
| 123 | 122 | fveqeq2d 6914 |
. . . . . . . . 9
⊢ (𝑗 = (𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒)))) → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘((𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒))))‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) |
| 124 | 123 | ralbidv 3178 |
. . . . . . . 8
⊢ (𝑗 = (𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒)))) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘((𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒))))‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) |
| 125 | 121, 124 | anbi12d 632 |
. . . . . . 7
⊢ (𝑗 = (𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒)))) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ↔ ((𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒)))):dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘((𝑒 ∈ dom (iEdg‘𝐺) ↦ (◡(iEdg‘𝐻)‘((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))‘((iEdg‘𝐺)‘𝑒))))‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))))) |
| 126 | 118, 120,
125 | spcedv 3598 |
. . . . . 6
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)):𝐸–1-1-onto→𝐷) → ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) |
| 127 | 126 | ex 412 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) → ((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)):𝐸–1-1-onto→𝐷 → ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))))) |
| 128 | 114, 127 | impbid 212 |
. . . 4
⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ↔ (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)):𝐸–1-1-onto→𝐷)) |
| 129 | | f1oeq1 6836 |
. . . . 5
⊢ ((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)) = (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) → ((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)):𝐸–1-1-onto→𝐷 ↔ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) |
| 130 | 110, 129 | mp1i 13 |
. . . 4
⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) → ((𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)):𝐸–1-1-onto→𝐷 ↔ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) |
| 131 | 128, 130 | bitrd 279 |
. . 3
⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ↔ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) |
| 132 | 131 | pm5.32da 579 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → ((𝐹:𝑉–1-1-onto→𝑊 ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷))) |
| 133 | 5, 132 | bitrd 279 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷))) |