Step | Hyp | Ref
| Expression |
1 | | grimdmrel 47803 |
. . . 4
⊢ Rel dom
GraphIso |
2 | 1 | ovrcl 7471 |
. . 3
⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐺 ∈ V ∧ 𝐻 ∈ V)) |
3 | 2 | 3ad2ant2 1133 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ∈ V ∧ 𝐻 ∈ V)) |
4 | | uhgrimisgrgric.v |
. . . . . . . . 9
⊢ 𝑉 = (Vtx‘𝐺) |
5 | | eqid 2734 |
. . . . . . . . 9
⊢
(Vtx‘𝐻) =
(Vtx‘𝐻) |
6 | | eqid 2734 |
. . . . . . . . 9
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
7 | | eqid 2734 |
. . . . . . . . 9
⊢
(iEdg‘𝐻) =
(iEdg‘𝐻) |
8 | 4, 5, 6, 7 | grimprop 47806 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))))) |
9 | | f1ofun 6850 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → Fun 𝐹) |
10 | 9 | 3ad2ant1 1132 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → Fun 𝐹) |
11 | 4 | fvexi 6920 |
. . . . . . . . . . . . . . 15
⊢ 𝑉 ∈ V |
12 | 11 | ssex 5326 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ⊆ 𝑉 → 𝑁 ∈ V) |
13 | | resfunexg 7234 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐹 ∧ 𝑁 ∈ V) → (𝐹 ↾ 𝑁) ∈ V) |
14 | 10, 12, 13 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐹 ↾ 𝑁) ∈ V) |
15 | | f1of1 6847 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉–1-1→(Vtx‘𝐻)) |
16 | 15 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → 𝐹:𝑉–1-1→(Vtx‘𝐻)) |
17 | | f1ores 6862 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝑉–1-1→(Vtx‘𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) |
18 | 16, 17 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) |
19 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) |
20 | | vex 3481 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑔 ∈ V |
21 | 20 | resex 6048 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ∈ V |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ∈ V) |
23 | | f1of1 6847 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) → 𝑔:dom (iEdg‘𝐺)–1-1→dom (iEdg‘𝐻)) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → 𝑔:dom (iEdg‘𝐺)–1-1→dom (iEdg‘𝐻)) |
25 | 24 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → 𝑔:dom (iEdg‘𝐺)–1-1→dom (iEdg‘𝐻)) |
26 | 25 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → 𝑔:dom (iEdg‘𝐺)–1-1→dom (iEdg‘𝐻)) |
27 | | ssrab2 4089 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺) |
28 | | f1ores 6862 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔:dom (iEdg‘𝐺)–1-1→dom (iEdg‘𝐻) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)) → (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→(𝑔 “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})) |
29 | 26, 27, 28 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→(𝑔 “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})) |
30 | 4, 6 | uhgrf 29093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐺 ∈ UHGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅})) |
31 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖
{∅})) |
32 | | difssd 4146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (𝒫 𝑉 ∖ {∅}) ⊆
𝒫 𝑉) |
33 | 31, 32 | fssd 6753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉) |
34 | 30, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 ∈ UHGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶𝒫 𝑉) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶𝒫 𝑉) |
36 | 35 | anim2i 617 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)) |
37 | 36 | 3adant2 1130 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)) |
38 | 37 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)) |
39 | | simp2l 1198 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) |
40 | 39 | anim1i 615 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧ 𝑁 ⊆ 𝑉)) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧ 𝑁 ⊆ 𝑉)) |
42 | 41 | ancomd 461 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → (𝑁 ⊆ 𝑉 ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻))) |
43 | | simpl2r 1226 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) |
44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) |
45 | | uhgrimisgrgriclem 47835 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝑗 ∈ dom (iEdg‘𝐻) ∧ ((iEdg‘𝐻)‘𝑗) ⊆ (𝐹 “ 𝑁)) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)(((iEdg‘𝐺)‘𝑘) ⊆ 𝑁 ∧ (𝑔‘𝑘) = 𝑗))) |
46 | 38, 42, 44, 45 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → ((𝑗 ∈ dom (iEdg‘𝐻) ∧ ((iEdg‘𝐻)‘𝑗) ⊆ (𝐹 “ 𝑁)) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)(((iEdg‘𝐺)‘𝑘) ⊆ 𝑁 ∧ (𝑔‘𝑘) = 𝑗))) |
47 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑘 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝑘)) |
48 | 47 | sseq1d 4026 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑘 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘𝑘) ⊆ 𝑁)) |
49 | 48 | rexrab 3704 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑘 ∈
{𝑥 ∈ dom
(iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑔‘𝑘) = 𝑗 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)(((iEdg‘𝐺)‘𝑘) ⊆ 𝑁 ∧ (𝑔‘𝑘) = 𝑗)) |
50 | 46, 49 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → ((𝑗 ∈ dom (iEdg‘𝐻) ∧ ((iEdg‘𝐻)‘𝑗) ⊆ (𝐹 “ 𝑁)) ↔ ∃𝑘 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑔‘𝑘) = 𝑗)) |
51 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑗 → ((iEdg‘𝐻)‘𝑥) = ((iEdg‘𝐻)‘𝑗)) |
52 | 51 | sseq1d 4026 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑗 → (((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁) ↔ ((iEdg‘𝐻)‘𝑗) ⊆ (𝐹 “ 𝑁))) |
53 | 52 | elrab 3694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ↔ (𝑗 ∈ dom (iEdg‘𝐻) ∧ ((iEdg‘𝐻)‘𝑗) ⊆ (𝐹 “ 𝑁))) |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → (𝑗 ∈ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ↔ (𝑗 ∈ dom (iEdg‘𝐻) ∧ ((iEdg‘𝐻)‘𝑗) ⊆ (𝐹 “ 𝑁)))) |
55 | | f1ofn 6849 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) → 𝑔 Fn dom (iEdg‘𝐺)) |
56 | 55, 27 | jctir 520 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) →
(𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺))) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺))) |
58 | 57 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺))) |
59 | 58 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → (𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺))) |
60 | | fvelimab 6980 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)) → (𝑗 ∈ (𝑔 “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ↔ ∃𝑘 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑔‘𝑘) = 𝑗)) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → (𝑗 ∈ (𝑔 “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ↔ ∃𝑘 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑔‘𝑘) = 𝑗)) |
62 | 50, 54, 61 | 3bitr4d 311 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → (𝑗 ∈ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ↔ 𝑗 ∈ (𝑔 “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}))) |
63 | 62 | eqrdv 2732 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} = (𝑔 “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})) |
64 | 63 | f1oeq3d 6845 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → ((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ↔ (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→(𝑔 “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}))) |
65 | 29, 64 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)}) |
66 | | ssralv 4063 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ({𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) |
67 | 27, 66 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑖 ∈
dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) |
68 | | elex 3498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐺 ∈ UHGraph → 𝐺 ∈ V) |
69 | 68 | anim1i 615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝐺 ∈ V ∧ 𝐻 ∈ V)) |
70 | 69 | 3anim3i 1153 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V))) |
71 | 70 | anim1i 615 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉)) |
72 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) |
73 | | fvres 6925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} → ((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖) = (𝑔‘𝑖)) |
74 | 73 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖) = (𝑔‘𝑖)) |
75 | 74 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))) |
76 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 = 𝑖 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝑖)) |
77 | 76 | sseq1d 4026 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 = 𝑖 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁)) |
78 | 77 | elrab 3694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ↔ (𝑖 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁)) |
79 | 78 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} → ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁) |
80 | 79 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁) |
81 | | resima2 6035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((iEdg‘𝐺)‘𝑖) ⊆ 𝑁 → ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) |
83 | 72, 75, 82 | 3eqtr4rd 2785 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))) |
84 | 83 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))) |
85 | 71, 84 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧ 𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))) |
86 | 85 | ralimdva 3164 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) →
(∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))) |
87 | 67, 86 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) →
(∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))) |
88 | 87 | expimpd 453 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))) |
89 | 88 | 3exp1 1351 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → ((𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))))) |
90 | 89 | com25 99 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → ((𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))))) |
91 | 90 | 3imp1 1346 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → ((𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))) |
92 | 91 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))) |
93 | 65, 92 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → ((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))) |
94 | | f1oeq1 6836 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ↔ (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)})) |
95 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (ℎ‘𝑖) = ((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)) |
96 | 95 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → ((iEdg‘𝐻)‘(ℎ‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))) |
97 | 96 | eqeq2d 2745 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))) |
98 | 97 | ralbidv 3175 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))) |
99 | 94, 98 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → ((ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) ↔ ((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}):{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))) |
100 | 22, 93, 99 | spcedv 3597 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) |
101 | 19, 100 | jca 511 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)) → ((𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))) |
102 | 18, 101 | mpdan 687 |
. . . . . . . . . . . . 13
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → ((𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))) |
103 | | f1oeq1 6836 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝐹 ↾ 𝑁) → (𝑓:𝑁–1-1-onto→(𝐹 “ 𝑁) ↔ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁))) |
104 | | imaeq1 6074 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝐹 ↾ 𝑁) → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖))) |
105 | 104 | eqeq1d 2736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝐹 ↾ 𝑁) → ((𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) |
106 | 105 | ralbidv 3175 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝐹 ↾ 𝑁) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) |
107 | 106 | anbi2d 630 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝐹 ↾ 𝑁) → ((ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) ↔ (ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))) |
108 | 107 | exbidv 1918 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝐹 ↾ 𝑁) → (∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) ↔ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))) |
109 | 103, 108 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝐹 ↾ 𝑁) → ((𝑓:𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))) ↔ ((𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))))) |
110 | 14, 102, 109 | spcedv 3597 |
. . . . . . . . . . . 12
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → ∃𝑓(𝑓:𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))) |
111 | | simpl3 1192 |
. . . . . . . . . . . . 13
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) |
112 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → 𝑁 ⊆ 𝑉) |
113 | | f1of 6848 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉⟶(Vtx‘𝐻)) |
114 | 113 | fimassd 6757 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻)) |
115 | 114 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (𝑁 ⊆ 𝑉 → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻))) |
116 | 115 | 3ad2ant1 1132 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝑁 ⊆ 𝑉 → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻))) |
117 | 116 | imp 406 |
. . . . . . . . . . . . 13
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻)) |
118 | | eqid 2734 |
. . . . . . . . . . . . . 14
⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} |
119 | | eqid 2734 |
. . . . . . . . . . . . . 14
⊢ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} |
120 | 4, 5, 6, 7, 118, 119 | isubgrgrim 47834 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) ∧ (𝑁 ⊆ 𝑉 ∧ (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻))) → ((𝐺 ISubGr 𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ 𝑁)) ↔ ∃𝑓(𝑓:𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))))) |
121 | 111, 112,
117, 120 | syl12anc 837 |
. . . . . . . . . . . 12
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → ((𝐺 ISubGr 𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ 𝑁)) ↔ ∃𝑓(𝑓:𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ ∃ℎ(ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)))))) |
122 | 110, 121 | mpbird 257 |
. . . . . . . . . . 11
⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ISubGr 𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ 𝑁))) |
123 | 122 | 3exp1 1351 |
. . . . . . . . . 10
⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ 𝑁)))))) |
124 | 123 | exlimdv 1930 |
. . . . . . . . 9
⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ 𝑁)))))) |
125 | 124 | imp 406 |
. . . . . . . 8
⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ 𝑁))))) |
126 | 8, 125 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ 𝑁))))) |
127 | 126 | expd 415 |
. . . . . 6
⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐺 ∈ UHGraph → (𝐻 ∈ V → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ 𝑁)))))) |
128 | 127 | com12 32 |
. . . . 5
⊢ (𝐺 ∈ UHGraph → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐻 ∈ V → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ 𝑁)))))) |
129 | 128 | com34 91 |
. . . 4
⊢ (𝐺 ∈ UHGraph → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝑁 ⊆ 𝑉 → (𝐻 ∈ V → (𝐺 ISubGr 𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ 𝑁)))))) |
130 | 129 | 3imp 1110 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐻 ∈ V → (𝐺 ISubGr 𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ 𝑁)))) |
131 | 130 | adantld 490 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → ((𝐺 ∈ V ∧ 𝐻 ∈ V) → (𝐺 ISubGr 𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ 𝑁)))) |
132 | 3, 131 | mpd 15 |
1
⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ISubGr 𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ 𝑁))) |