| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . . 7
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
| 2 | | eqid 2737 |
. . . . . . 7
⊢
(Vtx‘𝑇) =
(Vtx‘𝑇) |
| 3 | | eqid 2737 |
. . . . . . 7
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
| 4 | | eqid 2737 |
. . . . . . 7
⊢
(iEdg‘𝑇) =
(iEdg‘𝑇) |
| 5 | 1, 2, 3, 4 | grimprop 47869 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))))) |
| 6 | | fdmrn 6767 |
. . . . . . . . . . . . . 14
⊢ (Fun
(iEdg‘𝑇) ↔
(iEdg‘𝑇):dom
(iEdg‘𝑇)⟶ran
(iEdg‘𝑇)) |
| 7 | 6 | biimpi 216 |
. . . . . . . . . . . . 13
⊢ (Fun
(iEdg‘𝑇) →
(iEdg‘𝑇):dom
(iEdg‘𝑇)⟶ran
(iEdg‘𝑇)) |
| 8 | 7 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) ∧ Fun (iEdg‘𝑇)) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶ran (iEdg‘𝑇)) |
| 9 | 8 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) ∧ Fun (iEdg‘𝑇)) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) →
(iEdg‘𝑇):dom
(iEdg‘𝑇)⟶ran
(iEdg‘𝑇)) |
| 10 | | funfn 6596 |
. . . . . . . . . . . . . 14
⊢ (Fun
(iEdg‘𝑇) ↔
(iEdg‘𝑇) Fn dom
(iEdg‘𝑇)) |
| 11 | 10 | biimpi 216 |
. . . . . . . . . . . . 13
⊢ (Fun
(iEdg‘𝑇) →
(iEdg‘𝑇) Fn dom
(iEdg‘𝑇)) |
| 12 | 11 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) ∧ Fun (iEdg‘𝑇)) → (iEdg‘𝑇) Fn dom (iEdg‘𝑇)) |
| 13 | | f1ofo 6855 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) → 𝑗:dom (iEdg‘𝑆)–onto→dom (iEdg‘𝑇)) |
| 14 | 13 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) →
𝑗:dom (iEdg‘𝑆)–onto→dom (iEdg‘𝑇)) |
| 15 | 14 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) → 𝑗:dom (iEdg‘𝑆)–onto→dom (iEdg‘𝑇)) |
| 16 | | foelcdmi 6970 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗:dom (iEdg‘𝑆)–onto→dom (iEdg‘𝑇) ∧ 𝑥 ∈ dom (iEdg‘𝑇)) → ∃𝑦 ∈ dom (iEdg‘𝑆)(𝑗‘𝑦) = 𝑥) |
| 17 | 15, 16 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) ∧ 𝑥 ∈ dom (iEdg‘𝑇)) → ∃𝑦 ∈ dom (iEdg‘𝑆)(𝑗‘𝑦) = 𝑥) |
| 18 | 17 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) → (𝑥 ∈ dom (iEdg‘𝑇) → ∃𝑦 ∈ dom (iEdg‘𝑆)(𝑗‘𝑦) = 𝑥)) |
| 19 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 = 𝑦 → ((iEdg‘𝑇)‘(𝑗‘𝑖)) = ((iEdg‘𝑇)‘(𝑗‘𝑦))) |
| 20 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 = 𝑦 → ((iEdg‘𝑆)‘𝑖) = ((iEdg‘𝑆)‘𝑦)) |
| 21 | 20 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 = 𝑦 → (𝐹 “ ((iEdg‘𝑆)‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))) |
| 22 | 19, 21 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 = 𝑦 → (((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) ↔ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)))) |
| 23 | 22 | rspcv 3618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ dom (iEdg‘𝑆) → (∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)))) |
| 24 | 23 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)))) |
| 25 | | f1ofun 6850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → Fun 𝐹) |
| 26 | 25 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → Fun
𝐹) |
| 27 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) → Fun
𝐹) |
| 28 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((iEdg‘𝑆)‘𝑦) ∈ V |
| 29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑦) ∈ V) |
| 30 | | funimaexg 6653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((Fun
𝐹 ∧ ((iEdg‘𝑆)‘𝑦) ∈ V) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ V) |
| 31 | 27, 29, 30 | syl2an2r 685 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ V) |
| 32 | | f1of 6848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → 𝐹:(Vtx‘𝑆)⟶(Vtx‘𝑇)) |
| 33 | 32 | fimassd 6757 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ⊆ (Vtx‘𝑇)) |
| 34 | 33 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) →
(𝐹 “
((iEdg‘𝑆)‘𝑦)) ⊆ (Vtx‘𝑇)) |
| 35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) →
(𝐹 “
((iEdg‘𝑆)‘𝑦)) ⊆ (Vtx‘𝑇)) |
| 36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ⊆ (Vtx‘𝑇)) |
| 37 | 31, 36 | elpwd 4606 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ 𝒫 (Vtx‘𝑇)) |
| 38 | | f1odm 6852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → dom 𝐹 = (Vtx‘𝑆)) |
| 39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → dom
𝐹 = (Vtx‘𝑆)) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧
𝑦 ∈ dom
(iEdg‘𝑆)) → dom
𝐹 = (Vtx‘𝑆)) |
| 41 | 40 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧
𝑦 ∈ dom
(iEdg‘𝑆)) → (dom
𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) = ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦))) |
| 42 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖
{∅})) |
| 43 | 42 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) →
(𝑦 ∈ dom
(iEdg‘𝑆) →
((iEdg‘𝑆)‘𝑦) ∈ (𝒫
(Vtx‘𝑆) ∖
{∅}))) |
| 44 | 43 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) →
(𝑦 ∈ dom
(iEdg‘𝑆) →
((iEdg‘𝑆)‘𝑦) ∈ (𝒫
(Vtx‘𝑆) ∖
{∅}))) |
| 45 | | eldifsn 4786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ↔
(((iEdg‘𝑆)‘𝑦) ∈ 𝒫 (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅)) |
| 46 | 28 | elpw 4604 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((iEdg‘𝑆)‘𝑦) ∈ 𝒫 (Vtx‘𝑆) ↔ ((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆)) |
| 47 | 45, 46 | bianbi 627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ↔
(((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅)) |
| 48 | | sseqin2 4223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
(((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ↔ ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) = ((iEdg‘𝑆)‘𝑦)) |
| 49 | 48 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) = ((iEdg‘𝑆)‘𝑦)) |
| 50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
((((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) = ((iEdg‘𝑆)‘𝑦)) |
| 51 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
((((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅) → ((iEdg‘𝑆)‘𝑦) ≠ ∅) |
| 52 | 50, 51 | eqnetrd 3008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
((((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅) |
| 53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) →
((((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅)) |
| 54 | 47, 53 | biimtrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) →
(((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) →
((Vtx‘𝑆) ∩
((iEdg‘𝑆)‘𝑦)) ≠
∅)) |
| 55 | 44, 54 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) →
(𝑦 ∈ dom
(iEdg‘𝑆) →
((Vtx‘𝑆) ∩
((iEdg‘𝑆)‘𝑦)) ≠
∅)) |
| 56 | 55 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧
𝑦 ∈ dom
(iEdg‘𝑆)) →
((Vtx‘𝑆) ∩
((iEdg‘𝑆)‘𝑦)) ≠
∅) |
| 57 | 41, 56 | eqnetrd 3008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧
𝑦 ∈ dom
(iEdg‘𝑆)) → (dom
𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅) |
| 58 | 57 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) →
(𝑦 ∈ dom
(iEdg‘𝑆) → (dom
𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅)) |
| 59 | 58 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) →
(𝑦 ∈ dom
(iEdg‘𝑆) → (dom
𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅)) |
| 60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) →
(𝑦 ∈ dom
(iEdg‘𝑆) → (dom
𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅)) |
| 61 | 60 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (dom 𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅) |
| 62 | 61 | imadisjlnd 6099 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ≠ ∅) |
| 63 | | eldifsn 4786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅}) ↔
((𝐹 “
((iEdg‘𝑆)‘𝑦)) ∈ 𝒫
(Vtx‘𝑇) ∧ (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ≠ ∅)) |
| 64 | 37, 62, 63 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅})) |
| 65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅})) |
| 66 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)) → (((iEdg‘𝑇)‘(𝑗‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅}) ↔
(𝐹 “
((iEdg‘𝑆)‘𝑦)) ∈ (𝒫
(Vtx‘𝑇) ∖
{∅}))) |
| 67 | 66 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))) → (((iEdg‘𝑇)‘(𝑗‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅}) ↔
(𝐹 “
((iEdg‘𝑆)‘𝑦)) ∈ (𝒫
(Vtx‘𝑇) ∖
{∅}))) |
| 68 | 65, 67 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))) → ((iEdg‘𝑇)‘(𝑗‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅})) |
| 69 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘(𝑗‘𝑦)) = ((iEdg‘𝑇)‘𝑥)) |
| 70 | 69 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗‘𝑦) = 𝑥 → (((iEdg‘𝑇)‘(𝑗‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅}) ↔
((iEdg‘𝑇)‘𝑥) ∈ (𝒫
(Vtx‘𝑇) ∖
{∅}))) |
| 71 | 68, 70 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))) → ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅}))) |
| 72 | 71 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)) → ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅})))) |
| 73 | 24, 72 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅})))) |
| 74 | 73 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) →
(𝑦 ∈ dom
(iEdg‘𝑆) →
(∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅}))))) |
| 75 | 74 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇)) →
(∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → (𝑦 ∈ dom (iEdg‘𝑆) → ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅}))))) |
| 76 | 75 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) →
(Fun (iEdg‘𝑇) →
(∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → (𝑦 ∈ dom (iEdg‘𝑆) → ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅})))))) |
| 77 | 76 | 3imp 1111 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) → (𝑦 ∈ dom (iEdg‘𝑆) → ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅})))) |
| 78 | 77 | rexlimdv 3153 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) → (∃𝑦 ∈ dom (iEdg‘𝑆)(𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅}))) |
| 79 | 18, 78 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) → (𝑥 ∈ dom (iEdg‘𝑇) → ((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅}))) |
| 80 | 79 | ralrimiv 3145 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) → ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅})) |
| 81 | 80 | 3exp 1120 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) →
(Fun (iEdg‘𝑇) →
(∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅})))) |
| 82 | 81 | 3exp 1120 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) →
((iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) → (Fun
(iEdg‘𝑇) →
(∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅})))))) |
| 83 | 82 | com35 98 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) →
(∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → (Fun (iEdg‘𝑇) → ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) →
∀𝑥 ∈ dom
(iEdg‘𝑇)((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅})))))) |
| 84 | 83 | impd 410 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → ((𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) → (Fun (iEdg‘𝑇) → ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) →
∀𝑥 ∈ dom
(iEdg‘𝑇)((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅}))))) |
| 85 | 84 | 3imp 1111 |
. . . . . . . . . . . . 13
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) ∧ Fun (iEdg‘𝑇)) → ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) →
∀𝑥 ∈ dom
(iEdg‘𝑇)((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅}))) |
| 86 | 85 | imp 406 |
. . . . . . . . . . . 12
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) ∧ Fun (iEdg‘𝑇)) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) →
∀𝑥 ∈ dom
(iEdg‘𝑇)((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖
{∅})) |
| 87 | | fnfvrnss 7141 |
. . . . . . . . . . . 12
⊢
(((iEdg‘𝑇) Fn
dom (iEdg‘𝑇) ∧
∀𝑥 ∈ dom
(iEdg‘𝑇)((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅})) → ran
(iEdg‘𝑇) ⊆
(𝒫 (Vtx‘𝑇)
∖ {∅})) |
| 88 | 12, 86, 87 | syl2an2r 685 |
. . . . . . . . . . 11
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) ∧ Fun (iEdg‘𝑇)) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → ran
(iEdg‘𝑇) ⊆
(𝒫 (Vtx‘𝑇)
∖ {∅})) |
| 89 | 9, 88 | fssd 6753 |
. . . . . . . . . 10
⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) ∧ Fun (iEdg‘𝑇)) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) →
(iEdg‘𝑇):dom
(iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖
{∅})) |
| 90 | 89 | ex 412 |
. . . . . . . . 9
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) ∧ Fun (iEdg‘𝑇)) → ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) →
(iEdg‘𝑇):dom
(iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖
{∅}))) |
| 91 | 90 | 3exp 1120 |
. . . . . . . 8
⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → ((𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) → (Fun (iEdg‘𝑇) → ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) →
(iEdg‘𝑇):dom
(iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖
{∅}))))) |
| 92 | 91 | exlimdv 1933 |
. . . . . . 7
⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → (∃𝑗(𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) → (Fun (iEdg‘𝑇) → ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) →
(iEdg‘𝑇):dom
(iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖
{∅}))))) |
| 93 | 92 | imp 406 |
. . . . . 6
⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)–1-1-onto→dom
(iEdg‘𝑇) ∧
∀𝑖 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) → (Fun (iEdg‘𝑇) → ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫
(Vtx‘𝑆) ∖
{∅}) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖
{∅})))) |
| 94 | 5, 93 | syl 17 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (Fun (iEdg‘𝑇) → ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) →
(iEdg‘𝑇):dom
(iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖
{∅})))) |
| 95 | 94 | impcom 407 |
. . . 4
⊢ ((Fun
(iEdg‘𝑇) ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) → ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) →
(iEdg‘𝑇):dom
(iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖
{∅}))) |
| 96 | | grimdmrel 47866 |
. . . . . . 7
⊢ Rel dom
GraphIso |
| 97 | 96 | ovrcl 7472 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝑆 ∈ V ∧ 𝑇 ∈ V)) |
| 98 | 1, 3 | isuhgr 29077 |
. . . . . . . 8
⊢ (𝑆 ∈ V → (𝑆 ∈ UHGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖
{∅}))) |
| 99 | 98 | adantr 480 |
. . . . . . 7
⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑆 ∈ UHGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖
{∅}))) |
| 100 | 2, 4 | isuhgr 29077 |
. . . . . . . 8
⊢ (𝑇 ∈ V → (𝑇 ∈ UHGraph ↔
(iEdg‘𝑇):dom
(iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖
{∅}))) |
| 101 | 100 | adantl 481 |
. . . . . . 7
⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑇 ∈ UHGraph ↔
(iEdg‘𝑇):dom
(iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖
{∅}))) |
| 102 | 99, 101 | imbi12d 344 |
. . . . . 6
⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → ((𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph) ↔
((iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) →
(iEdg‘𝑇):dom
(iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖
{∅})))) |
| 103 | 97, 102 | syl 17 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → ((𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph) ↔ ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫
(Vtx‘𝑆) ∖
{∅}) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖
{∅})))) |
| 104 | 103 | adantl 481 |
. . . 4
⊢ ((Fun
(iEdg‘𝑇) ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) → ((𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph) ↔ ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫
(Vtx‘𝑆) ∖
{∅}) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖
{∅})))) |
| 105 | 95, 104 | mpbird 257 |
. . 3
⊢ ((Fun
(iEdg‘𝑇) ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) → (𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph)) |
| 106 | 105 | ex 412 |
. 2
⊢ (Fun
(iEdg‘𝑇) →
(𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph))) |
| 107 | 106 | 3imp31 1112 |
1
⊢ ((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇) ∧ Fun (iEdg‘𝑇)) → 𝑇 ∈ UHGraph) |