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 48514

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 48463	. . . 4 ⊢ Rel dom GraphIso
2	1	ovrcl 7432	. . 3 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐺 ∈ V ∧ 𝐻 ∈ V))
3	2	3ad2ant2 1146	. 2 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ∈ V ∧ 𝐻 ∈ V))
4		uhgrimisgrgric.v	. . . . . . . . 9 ⊢ 𝑉 = (Vtx‘𝐺)
5		eqid 2761	. . . . . . . . 9 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
6		eqid 2761	. . . . . . . . 9 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
7		eqid 2761	. . . . . . . . 9 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
8	4, 5, 6, 7	grimprop 48466	. . . . . . . 8 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
9		f1ofun 6803	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → Fun 𝐹)
10	9	3ad2ant1 1145	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → Fun 𝐹)
11	4	fvexi 6876	. . . . . . . . . . . . . . 15 ⊢ 𝑉 ∈ V
12	11	ssex 5274	. . . . . . . . . . . . . 14 ⊢ (𝑁 ⊆ 𝑉 → 𝑁 ∈ V)
13		resfunexg 7194	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐹 ∧ 𝑁 ∈ V) → (𝐹 ↾ 𝑁) ∈ V)
14	10, 12, 13	syl2an 605	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐹 ↾ 𝑁) ∈ V)
15		f1of1 6800	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
16	15	3ad2ant1 1145	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
17		f1ores 6816	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1→(Vtx‘𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁))
18	16, 17	sylan 589	. . . . . . . . . . . . . 14 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁))
19		simpr 488	. . . . . . . . . . . . . . 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 3457	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑔 ∈ V
21	20	resex 6011	. . . . . . . . . . . . . . . . 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 6800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑔:dom (iEdg‘𝐺)–1-1→dom (iEdg‘𝐻))
24	23	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → 𝑔:dom (iEdg‘𝐺)–1-1→dom (iEdg‘𝐻))
25	24	3ad2ant2 1146	. . . . . . . . . . . . . . . . . . . 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 736	. . . . . . . . . . . . . . . . . . 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 4031	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)
28		f1ores 6816	. . . . . . . . . . . . . . . . . . 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 595	. . . . . . . . . . . . . . . . . 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 29220	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐺 ∈ UHGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}))
31		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}))
32		difssd 4088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (𝒫 𝑉 ∖ {∅}) ⊆ 𝒫 𝑉)
33	31, 32	fssd 6704	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)
34	30, 33	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐺 ∈ UHGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)
35	34	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)
36	35	anim2i 626	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉))
37	36	3adant2 1143	. . . . . . . . . . . . . . . . . . . . . . . 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 736	. . . . . . . . . . . . . . . . . . . . . . 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 1212	. . . . . . . . . . . . . . . . . . . . . . . . . 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 624	. . . . . . . . . . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . . . . . . . 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 1240	. . . . . . . . . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . . . . . . . . . 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 48513	. . . . . . . . . . . . . . . . . . . . . . 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 1389	. . . . . . . . . . . . . . . . . . . . . 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 6862	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑘 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝑘))
48	47	sseq1d 3965	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑘 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘𝑘) ⊆ 𝑁))
49	48	rexrab 3657	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑘 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑔‘𝑘) = 𝑗 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)(((iEdg‘𝐺)‘𝑘) ⊆ 𝑁 ∧ (𝑔‘𝑘) = 𝑗))
50	46, 49	bitr4di 291	. . . . . . . . . . . . . . . . . . . . 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 6862	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑗 → ((iEdg‘𝐻)‘𝑥) = ((iEdg‘𝐻)‘𝑗))
52	51	sseq1d 3965	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑗 → (((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁) ↔ ((iEdg‘𝐻)‘𝑗) ⊆ (𝐹 “ 𝑁)))
53	52	elrab 3649	. . . . . . . . . . . . . . . . . . . . . 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 6802	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑔 Fn dom (iEdg‘𝐺))
56	55, 27	jctir 528	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → (𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)))
57	56	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)))
58	57	3ad2ant2 1146	. . . . . . . . . . . . . . . . . . . . . . 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 736	. . . . . . . . . . . . . . . . . . . . . 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 6934	. . . . . . . . . . . . . . . . . . . . . 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 313	. . . . . . . . . . . . . . . . . . . 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 2759	. . . . . . . . . . . . . . . . . . 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 6798	. . . . . . . . . . . . . . . . . 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 259	. . . . . . . . . . . . . . . . 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 4003	. . . . . . . . . . . . . . . . . . . . . . . 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 3474	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐺 ∈ UHGraph → 𝐺 ∈ V)
69	68	anim1i 624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝐺 ∈ V ∧ 𝐻 ∈ V))
70	69	3anim3i 1166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)))
71	70	anim1i 624	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉))
72		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 6881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} → ((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖) = (𝑔‘𝑖))
74	73	ad2antlr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6866	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 6862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 = 𝑖 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝑖))
77	76	sseq1d 3965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 = 𝑖 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
78	77	elrab 3649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ↔ (𝑖 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
79	78	simprbi 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} → ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁)
80	79	ad2antlr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5998	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2807	. . . . . . . . . . . . . . . . . . . . . . . . . 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 416	. . . . . . . . . . . . . . . . . . . . . . . . 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 690	. . . . . . . . . . . . . . . . . . . . . . . 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 3173	. . . . . . . . . . . . . . . . . . . . . . 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 457	. . . . . . . . . . . . . . . . . . . . 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 1365	. . . . . . . . . . . . . . . . . . . 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 1360	. . . . . . . . . . . . . . . . . 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 410	. . . . . . . . . . . . . . . . 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 519	. . . . . . . . . . . . . . . 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 6789	. . . . . . . . . . . . . . . . 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 6861	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (ℎ‘𝑖) = ((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))
96	95	fveq2d 6866	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → ((iEdg‘𝐻)‘(ℎ‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))
97	96	eqeq2d 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
98	97	ralbidv 3184	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
99	94, 98	anbi12d 641	. . . . . . . . . . . . . . . 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 3556	. . . . . . . . . . . . . . 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 519	. . . . . . . . . . . . . 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 697	. . . . . . . . . . . . 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 6789	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝐹 ↾ 𝑁) → (𝑓:𝑁–1-1-onto→(𝐹 “ 𝑁) ↔ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)))
104		imaeq1 6040	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝐹 ↾ 𝑁) → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)))
105	104	eqeq1d 2763	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝐹 ↾ 𝑁) → ((𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))
106	105	ralbidv 3184	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝐹 ↾ 𝑁) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))
107	106	anbi2d 639	. . . . . . . . . . . . . . 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 1940	. . . . . . . . . . . . . 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 641	. . . . . . . . . . . . 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 3556	. . . . . . . . . . . 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 1206	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V))
112		simpr 488	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → 𝑁 ⊆ 𝑉)
113		f1of 6801	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉⟶(Vtx‘𝐻))
114	113	fimassd 6708	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻))
115	114	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (𝑁 ⊆ 𝑉 → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻)))
116	115	3ad2ant1 1145	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝑁 ⊆ 𝑉 → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻)))
117	116	imp 410	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻))
118		eqid 2761	. . . . . . . . . . . . . 14 ⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}
119		eqid 2761	. . . . . . . . . . . . . 14 ⊢ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)}
120	4, 5, 6, 7, 118, 119	isubgrgrim 48512	. . . . . . . . . . . . 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 847	. . . . . . . . . . . 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 259	. . . . . . . . . . 11 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁)))
123	122	3exp1 1365	. . . . . . . . . 10 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))))
124	123	exlimdv 1952	. . . . . . . . 9 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))))
125	124	imp 410	. . . . . . . 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 419	. . . . . 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 1122	. . 3 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐻 ∈ V → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))
131	130	adantld 494	. 2 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → ((𝐺 ∈ V ∧ 𝐻 ∈ V) → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))
132	3, 131	mpd 15	1 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1097 = wceq 1559 ∃wex 1798 ∈ wcel 2141 ∀wral 3075 ∃wrex 3085 {crab 3413 Vcvv 3453 ∖ cdif 3899 ⊆ wss 3902 ∅c0 4283 𝒫 cpw 4552 {csn 4579 class class class wbr 5097 dom cdm 5643 ↾ cres 5645 “ cima 5646 Fun wfun 6510 Fn wfn 6511 ⟶wf 6512 –1-1→wf1 6513 –1-1-onto→wf1o 6515 ‘cfv 6516 (class class class)co 7391 Vtxcvtx 29154 iEdgciedg 29155 UHGraphcuhgr 29214 ISubGr cisubgr 48443 GraphIso cgrim 48458 ≃_𝑔𝑟 cgric 48459

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3076 df-rex 3086 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-id 5538 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-ov 7394 df-oprab 7395 df-mpo 7396 df-1st 7965 df-2nd 7966 df-1o 8431 df-map 8804 df-vtx 29156 df-iedg 29157 df-uhgr 29216 df-isubgr 48444 df-grim 48461 df-gric 48464

This theorem is referenced by: uhgrimgrlim 48570

W3C validator