Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  uhgrimisgrgric Structured version   Visualization version   GIF version

Theorem uhgrimisgrgric 47899
Description: For isomorphic hypergraphs, the induced subgraph of a subset of vertices of one graph is isomorphic to the subgraph induced by the image of the subset. (Contributed by AV, 31-May-2025.)
Hypothesis
Ref Expression
uhgrimisgrgric.v 𝑉 = (Vtx‘𝐺)
Assertion
Ref Expression
uhgrimisgrgric ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁𝑉) → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹𝑁)))

Proof of Theorem uhgrimisgrgric
Dummy variables 𝑓 𝑖 𝑥 𝑔 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 grimdmrel 47866 . . . 4 Rel dom GraphIso
21ovrcl 7472 . . 3 (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐺 ∈ V ∧ 𝐻 ∈ V))
323ad2ant2 1135 . 2 ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁𝑉) → (𝐺 ∈ V ∧ 𝐻 ∈ V))
4 uhgrimisgrgric.v . . . . . . . . 9 𝑉 = (Vtx‘𝐺)
5 eqid 2737 . . . . . . . . 9 (Vtx‘𝐻) = (Vtx‘𝐻)
6 eqid 2737 . . . . . . . . 9 (iEdg‘𝐺) = (iEdg‘𝐺)
7 eqid 2737 . . . . . . . . 9 (iEdg‘𝐻) = (iEdg‘𝐻)
84, 5, 6, 7grimprop 47869 . . . . . . . 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 𝐹)
1093ad2ant1 1134 . . . . . . . . . . . . . 14 ((𝐹:𝑉1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → Fun 𝐹)
114fvexi 6920 . . . . . . . . . . . . . . 15 𝑉 ∈ V
1211ssex 5321 . . . . . . . . . . . . . 14 (𝑁𝑉𝑁 ∈ V)
13 resfunexg 7235 . . . . . . . . . . . . . 14 ((Fun 𝐹𝑁 ∈ V) → (𝐹𝑁) ∈ V)
1410, 12, 13syl2an 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‘𝐻))
16153ad2ant1 1134 . . . . . . . . . . . . . . 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→(𝐹𝑁))
1816, 17sylan 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 3484 . . . . . . . . . . . . . . . . . 18 𝑔 ∈ V
2120resex 6047 . . . . . . . . . . . . . . . . 17 (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ∈ V
2221a1i 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‘𝐻))
2423adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → 𝑔:dom (iEdg‘𝐺)–1-1→dom (iEdg‘𝐻))
25243ad2ant2 1135 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:𝑉1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → 𝑔:dom (iEdg‘𝐺)–1-1→dom (iEdg‘𝐻))
2625ad2antrr 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 4080 . . . . . . . . . . . . . . . . . . 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‘𝐺)‘𝑥) ⊆ 𝑁}))
2926, 27, 28sylancl 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‘𝐺)‘𝑥) ⊆ 𝑁}))
304, 6uhgrf 29079 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐺 ∈ UHGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}))
31 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}))
32 difssd 4137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (𝒫 𝑉 ∖ {∅}) ⊆ 𝒫 𝑉)
3331, 32fssd 6753 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)
3430, 33syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 ∈ UHGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)
3534adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)
3635anim2i 617 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹:𝑉1-1-onto→(Vtx‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝐹:𝑉1-1-onto→(Vtx‘𝐻) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉))
37363adant2 1132 . . . . . . . . . . . . . . . . . . . . . . . 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‘𝐺)⟶𝒫 𝑉))
3837ad2antrr 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 1200 . . . . . . . . . . . . . . . . . . . . . . . . . 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‘𝐻))
4039anim1i 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‘𝐻) ∧ 𝑁𝑉))
4140adantr 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‘𝐻) ∧ 𝑁𝑉))
4241ancomd 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 1228 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹:𝑉1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁𝑉) → ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))
4443adantr 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 47898 . . . . . . . . . . . . . . . . . . . . . . 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‘𝐺)‘𝑘) ⊆ 𝑁 ∧ (𝑔𝑘) = 𝑗)))
4638, 42, 44, 45syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . 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‘𝐺)‘𝑘))
4847sseq1d 4015 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑘 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘𝑘) ⊆ 𝑁))
4948rexrab 3702 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑘 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑔𝑘) = 𝑗 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)(((iEdg‘𝐺)‘𝑘) ⊆ 𝑁 ∧ (𝑔𝑘) = 𝑗))
5046, 49bitr4di 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‘𝐻)‘𝑗))
5251sseq1d 4015 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑗 → (((iEdg‘𝐻)‘𝑥) ⊆ (𝐹𝑁) ↔ ((iEdg‘𝐻)‘𝑗) ⊆ (𝐹𝑁)))
5352elrab 3692 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹𝑁)} ↔ (𝑗 ∈ dom (iEdg‘𝐻) ∧ ((iEdg‘𝐻)‘𝑗) ⊆ (𝐹𝑁)))
5453a1i 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‘𝐺))
5655, 27jctir 520 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → (𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)))
5756adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)))
58573ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . . . 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‘𝐺)))
5958ad2antrr 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 6981 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)) → (𝑗 ∈ (𝑔 “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ↔ ∃𝑘 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑔𝑘) = 𝑗))
6159, 60syl 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‘𝐺)‘𝑥) ⊆ 𝑁} (𝑔𝑘) = 𝑗))
6250, 54, 613bitr4d 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‘𝐺)‘𝑥) ⊆ 𝑁})))
6362eqrdv 2735 . . . . . . . . . . . . . . . . . . 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‘𝐺)‘𝑥) ⊆ 𝑁}))
6463f1oeq3d 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‘𝐺)‘𝑥) ⊆ 𝑁})))
6529, 64mpbird 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 4052 . . . . . . . . . . . . . . . . . . . . . . . 24 ({𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))))
6727, 66ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))
68 elex 3501 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐺 ∈ UHGraph → 𝐺 ∈ V)
6968anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝐺 ∈ V ∧ 𝐻 ∈ V))
70693anim3i 1155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹:𝑉1-1-onto→(Vtx‘𝐻) ∧ (𝐹𝑁):𝑁1-1-onto→(𝐹𝑁) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝐹:𝑉1-1-onto→(Vtx‘𝐻) ∧ (𝐹𝑁):𝑁1-1-onto→(𝐹𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)))
7170anim1i 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖) = (𝑔𝑖))
7473ad2antlr 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖) = (𝑔𝑖))
7574fveq2d 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‘𝐺)‘𝑖))
7776sseq1d 4015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = 𝑖 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
7877elrab 3692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ↔ (𝑖 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
7978simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} → ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁)
8079ad2antlr 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 6034 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((iEdg‘𝐺)‘𝑖) ⊆ 𝑁 → ((𝐹𝑁) “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))
8280, 81syl 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‘𝐺)‘𝑖)))
8372, 75, 823eqtr4rd 2788 . . . . . . . . . . . . . . . . . . . . . . . . . 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))
8483ex 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
8571, 84sylanl1 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
8685ralimdva 3167 . . . . . . . . . . . . . . . . . . . . . . 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
8767, 86syl5 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
8887expimpd 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
89883exp1 1353 . . . . . . . . . . . . . . . . . . . 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))))))
9089com25 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))))))
91903imp1 1348 . . . . . . . . . . . . . . . . . 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
9291imp 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))
9365, 92jca 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))
9695fveq2d 6910 . . . . . . . . . . . . . . . . . . 19 ( = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → ((iEdg‘𝐻)‘(𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))
9796eqeq2d 2748 . . . . . . . . . . . . . . . . . 18 ( = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (((𝐹𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖)) ↔ ((𝐹𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
9897ralbidv 3178 . . . . . . . . . . . . . . . . 17 ( = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖)) ↔ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
9994, 98anbi12d 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‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))))
10022, 93, 99spcedv 3598 . . . . . . . . . . . . . . 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‘𝐻)‘(𝑖))))
10119, 100jca 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‘𝐻)‘(𝑖)))))
10218, 101mpdan 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 6073 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝐹𝑁) → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((𝐹𝑁) “ ((iEdg‘𝐺)‘𝑖)))
105104eqeq1d 2739 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝐹𝑁) → ((𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖)) ↔ ((𝐹𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖))))
106105ralbidv 3178 . . . . . . . . . . . . . . . 16 (𝑓 = (𝐹𝑁) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖)) ↔ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖))))
107106anbi2d 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‘𝐻)‘(𝑖)))))
108107exbidv 1921 . . . . . . . . . . . . . 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‘𝐻)‘(𝑖)))))
109103, 108anbi12d 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‘𝐻)‘(𝑖))))))
11014, 102, 109spcedv 3598 . . . . . . . . . . . 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 1194 . . . . . . . . . . . . 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‘𝐻))
114113fimassd 6757 . . . . . . . . . . . . . . . 16 (𝐹:𝑉1-1-onto→(Vtx‘𝐻) → (𝐹𝑁) ⊆ (Vtx‘𝐻))
115114a1d 25 . . . . . . . . . . . . . . 15 (𝐹:𝑉1-1-onto→(Vtx‘𝐻) → (𝑁𝑉 → (𝐹𝑁) ⊆ (Vtx‘𝐻)))
1161153ad2ant1 1134 . . . . . . . . . . . . . 14 ((𝐹:𝑉1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝑁𝑉 → (𝐹𝑁) ⊆ (Vtx‘𝐻)))
117116imp 406 . . . . . . . . . . . . 13 (((𝐹:𝑉1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁𝑉) → (𝐹𝑁) ⊆ (Vtx‘𝐻))
118 eqid 2737 . . . . . . . . . . . . . 14 {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}
119 eqid 2737 . . . . . . . . . . . . . 14 {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹𝑁)} = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹𝑁)}
1204, 5, 6, 7, 118, 119isubgrgrim 47897 . . . . . . . . . . . . 13 (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) ∧ (𝑁𝑉 ∧ (𝐹𝑁) ⊆ (Vtx‘𝐻))) → ((𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹𝑁)) ↔ ∃𝑓(𝑓:𝑁1-1-onto→(𝐹𝑁) ∧ ∃(:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹𝑁)} ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖))))))
121111, 112, 117, 120syl12anc 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‘𝐻)‘(𝑖))))))
122110, 121mpbird 257 . . . . . . . . . . 11 (((𝐹:𝑉1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁𝑉) → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹𝑁)))
1231223exp1 1353 . . . . . . . . . 10 (𝐹:𝑉1-1-onto→(Vtx‘𝐻) → ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁𝑉 → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹𝑁))))))
124123exlimdv 1933 . . . . . . . . 9 (𝐹:𝑉1-1-onto→(Vtx‘𝐻) → (∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁𝑉 → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹𝑁))))))
125124imp 406 . . . . . . . 8 ((𝐹:𝑉1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁𝑉 → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹𝑁)))))
1268, 125syl 17 . . . . . . 7 (𝐹 ∈ (𝐺 GraphIso 𝐻) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁𝑉 → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹𝑁)))))
127126expd 415 . . . . . 6 (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐺 ∈ UHGraph → (𝐻 ∈ V → (𝑁𝑉 → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹𝑁))))))
128127com12 32 . . . . 5 (𝐺 ∈ UHGraph → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐻 ∈ V → (𝑁𝑉 → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹𝑁))))))
129128com34 91 . . . 4 (𝐺 ∈ UHGraph → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝑁𝑉 → (𝐻 ∈ V → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹𝑁))))))
1301293imp 1111 . . 3 ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁𝑉) → (𝐻 ∈ V → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹𝑁))))
131130adantld 490 . 2 ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁𝑉) → ((𝐺 ∈ V ∧ 𝐻 ∈ V) → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹𝑁))))
1323, 131mpd 15 1 ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁𝑉) → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wex 1779  wcel 2108  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  wss 3951  c0 4333  𝒫 cpw 4600  {csn 4626   class class class wbr 5143  dom cdm 5685  cres 5687  cima 5688  Fun wfun 6555   Fn wfn 6556  wf 6557  1-1wf1 6558  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  Vtxcvtx 29013  iEdgciedg 29014  UHGraphcuhgr 29073   ISubGr cisubgr 47846   GraphIso cgrim 47861  𝑔𝑟 cgric 47862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-1o 8506  df-map 8868  df-vtx 29015  df-iedg 29016  df-uhgr 29075  df-isubgr 47847  df-grim 47864  df-gric 47867
This theorem is referenced by:  uhgrimgrlim  47954
  Copyright terms: Public domain W3C validator