uhgrimisgrgric - Mathbox for Alexander van der Vekens

	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 48580

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.

Step	Hyp	Ref	Expression
1		grimdmrel 48529	. . . 4 ⊢ Rel dom GraphIso
2	1	ovrcl 7449	. . 3 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐺 ∈ V ∧ 𝐻 ∈ V))
3	2	3ad2ant2 1150	. 2 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ∈ V ∧ 𝐻 ∈ V))
4		uhgrimisgrgric.v	. . . . . . . . 9 ⊢ 𝑉 = (Vtx‘𝐺)
5		eqid 2769	. . . . . . . . 9 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
6		eqid 2769	. . . . . . . . 9 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
7		eqid 2769	. . . . . . . . 9 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
8	4, 5, 6, 7	grimprop 48532	. . . . . . . 8 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
9		f1ofun 6820	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → Fun 𝐹)
10	9	3ad2ant1 1149	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → Fun 𝐹)
11	4	fvexi 6893	. . . . . . . . . . . . . . 15 ⊢ 𝑉 ∈ V
12	11	ssex 5289	. . . . . . . . . . . . . 14 ⊢ (𝑁 ⊆ 𝑉 → 𝑁 ∈ V)
13		resfunexg 7211	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐹 ∧ 𝑁 ∈ V) → (𝐹 ↾ 𝑁) ∈ V)
14	10, 12, 13	syl2an 607	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐹 ↾ 𝑁) ∈ V)
15		f1of1 6817	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
16	15	3ad2ant1 1149	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
17		f1ores 6833	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1→(Vtx‘𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁))
18	16, 17	sylan 591	. . . . . . . . . . . . . 14 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁))
19		simpr 489	. . . . . . . . . . . . . . 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 3467	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑔 ∈ V
21	20	resex 6026	. . . . . . . . . . . . . . . . 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 6817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑔:dom (iEdg‘𝐺)–1-1→dom (iEdg‘𝐻))
24	23	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → 𝑔:dom (iEdg‘𝐺)–1-1→dom (iEdg‘𝐻))
25	24	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . 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 738	. . . . . . . . . . . . . . . . . . 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 4042	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)
28		f1ores 6833	. . . . . . . . . . . . . . . . . . 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 597	. . . . . . . . . . . . . . . . . 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 29349	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐺 ∈ UHGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}))
31		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}))
32		difssd 4099	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (𝒫 𝑉 ∖ {∅}) ⊆ 𝒫 𝑉)
33	31, 32	fssd 6721	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)
34	30, 33	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐺 ∈ UHGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)
35	34	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)
36	35	anim2i 628	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉))
37	36	3adant2 1147	. . . . . . . . . . . . . . . . . . . . . . . 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 738	. . . . . . . . . . . . . . . . . . . . . . 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 1216	. . . . . . . . . . . . . . . . . . . . . . . . . 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 626	. . . . . . . . . . . . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . . . . . . 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 1244	. . . . . . . . . . . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . . . . . . . . . . . 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 48579	. . . . . . . . . . . . . . . . . . . . . . 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 1396	. . . . . . . . . . . . . . . . . . . . . 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 6879	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑘 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝑘))
48	47	sseq1d 3976	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑘 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘𝑘) ⊆ 𝑁))
49	48	rexrab 3668	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑘 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑔‘𝑘) = 𝑗 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)(((iEdg‘𝐺)‘𝑘) ⊆ 𝑁 ∧ (𝑔‘𝑘) = 𝑗))
50	46, 49	bitr4di 292	. . . . . . . . . . . . . . . . . . . . 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 6879	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑗 → ((iEdg‘𝐻)‘𝑥) = ((iEdg‘𝐻)‘𝑗))
52	51	sseq1d 3976	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑗 → (((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁) ↔ ((iEdg‘𝐻)‘𝑗) ⊆ (𝐹 “ 𝑁)))
53	52	elrab 3659	. . . . . . . . . . . . . . . . . . . . . 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 6819	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑔 Fn dom (iEdg‘𝐺))
56	55, 27	jctir 529	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → (𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)))
57	56	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)))
58	57	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . . . . 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 738	. . . . . . . . . . . . . . . . . . . . . 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 6951	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)) → (𝑗 ∈ (𝑔 “ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ↔ ∃𝑘 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑔‘𝑘) = 𝑗))
61	59, 60	syl 18	. . . . . . . . . . . . . . . . . . . . 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 314	. . . . . . . . . . . . . . . . . . . 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 2767	. . . . . . . . . . . . . . . . . . 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 6815	. . . . . . . . . . . . . . . . . 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 260	. . . . . . . . . . . . . . . . 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 4014	. . . . . . . . . . . . . . . . . . . . . . . 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 3484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐺 ∈ UHGraph → 𝐺 ∈ V)
69	68	anim1i 626	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝐺 ∈ V ∧ 𝐻 ∈ V))
70	69	3anim3i 1170	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)))
71	70	anim1i 626	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉))
72		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 6898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} → ((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖) = (𝑔‘𝑖))
74	73	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6883	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 6879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 = 𝑖 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝑖))
77	76	sseq1d 3976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 = 𝑖 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
78	77	elrab 3659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ↔ (𝑖 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
79	78	simprbi 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} → ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁)
80	79	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6013	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((iEdg‘𝐺)‘𝑖) ⊆ 𝑁 → ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))
82	80, 81	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2815	. . . . . . . . . . . . . . . . . . . . . . . . . 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 417	. . . . . . . . . . . . . . . . . . . . . . . . 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 692	. . . . . . . . . . . . . . . . . . . . . . . 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 3183	. . . . . . . . . . . . . . . . . . . . . . 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 35	. . . . . . . . . . . . . . . . . . . . . 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 458	. . . . . . . . . . . . . . . . . . . . 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 1369	. . . . . . . . . . . . . . . . . . . 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 100	. . . . . . . . . . . . . . . . . . 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 1364	. . . . . . . . . . . . . . . . . 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 411	. . . . . . . . . . . . . . . . 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 520	. . . . . . . . . . . . . . . 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 6806	. . . . . . . . . . . . . . . . 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 6878	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (ℎ‘𝑖) = ((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))
96	95	fveq2d 6883	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → ((iEdg‘𝐻)‘(ℎ‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))
97	96	eqeq2d 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
98	97	ralbidv 3194	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
99	94, 98	anbi12d 643	. . . . . . . . . . . . . . . 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 3566	. . . . . . . . . . . . . . 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 520	. . . . . . . . . . . . . 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 699	. . . . . . . . . . . . 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 6806	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝐹 ↾ 𝑁) → (𝑓:𝑁–1-1-onto→(𝐹 “ 𝑁) ↔ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)))
104		imaeq1 6055	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝐹 ↾ 𝑁) → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)))
105	104	eqeq1d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝐹 ↾ 𝑁) → ((𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))
106	105	ralbidv 3194	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝐹 ↾ 𝑁) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))
107	106	anbi2d 641	. . . . . . . . . . . . . . 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 1948	. . . . . . . . . . . . . 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 643	. . . . . . . . . . . . 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 3566	. . . . . . . . . . . 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 1210	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V))
112		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → 𝑁 ⊆ 𝑉)
113		f1of 6818	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉⟶(Vtx‘𝐻))
114	113	fimassd 6725	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻))
115	114	a1d 26	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (𝑁 ⊆ 𝑉 → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻)))
116	115	3ad2ant1 1149	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝑁 ⊆ 𝑉 → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻)))
117	116	imp 411	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻))
118		eqid 2769	. . . . . . . . . . . . . 14 ⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}
119		eqid 2769	. . . . . . . . . . . . . 14 ⊢ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)}
120	4, 5, 6, 7, 118, 119	isubgrgrim 48578	. . . . . . . . . . . . 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 849	. . . . . . . . . . . 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 260	. . . . . . . . . . 11 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁)))
123	122	3exp1 1369	. . . . . . . . . 10 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))))
124	123	exlimdv 1960	. . . . . . . . 9 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))))
125	124	imp 411	. . . . . . . 8 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁)))))
126	8, 125	syl 18	. . . . . . 7 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁)))))
127	126	expd 420	. . . . . 6 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐺 ∈ UHGraph → (𝐻 ∈ V → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))))
128	127	com12 33	. . . . 5 ⊢ (𝐺 ∈ UHGraph → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐻 ∈ V → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))))
129	128	com34 92	. . . 4 ⊢ (𝐺 ∈ UHGraph → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝑁 ⊆ 𝑉 → (𝐻 ∈ V → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))))
130	129	3imp 1126	. . 3 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐻 ∈ V → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))
131	130	adantld 495	. 2 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → ((𝐺 ∈ V ∧ 𝐻 ∈ V) → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))
132	3, 131	mpd 16	1 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∃wex 1806 ∈ wcel 2149 ∀wral 3085 ∃wrex 3095 {crab 3423 Vcvv 3463 ∖ cdif 3910 ⊆ wss 3913 ∅c0 4294 𝒫 cpw 4564 {csn 4591 class class class wbr 5110 dom cdm 5659 ↾ cres 5661 “ cima 5662 Fun wfun 6528 Fn wfn 6529 ⟶wf 6530 –1-1→wf1 6531 –1-1-onto→wf1o 6533 ‘cfv 6534 (class class class)co 7408 Vtxcvtx 29283 iEdgciedg 29284 UHGraphcuhgr 29343 ISubGr cisubgr 48509 GraphIso cgrim 48524 ≃_𝑔𝑟 cgric 48525

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5239 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-id 5554 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-suc 6364 df-iota 6490 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-ov 7411 df-oprab 7412 df-mpo 7413 df-1st 7982 df-2nd 7983 df-1o 8449 df-map 8822 df-vtx 29285 df-iedg 29286 df-uhgr 29345 df-isubgr 48510 df-grim 48527 df-gric 48530

This theorem is referenced by: uhgrimgrlim 48636

W3C validator