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 48422

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 48371	. . . 4 ⊢ Rel dom GraphIso
2	1	ovrcl 7397	. . 3 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐺 ∈ V ∧ 𝐻 ∈ V))
3	2	3ad2ant2 1140	. 2 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ∈ V ∧ 𝐻 ∈ V))
4		uhgrimisgrgric.v	. . . . . . . . 9 ⊢ 𝑉 = (Vtx‘𝐺)
5		eqid 2739	. . . . . . . . 9 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
6		eqid 2739	. . . . . . . . 9 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
7		eqid 2739	. . . . . . . . 9 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
8	4, 5, 6, 7	grimprop 48374	. . . . . . . 8 ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
9		f1ofun 6769	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → Fun 𝐹)
10	9	3ad2ant1 1139	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → Fun 𝐹)
11	4	fvexi 6841	. . . . . . . . . . . . . . 15 ⊢ 𝑉 ∈ V
12	11	ssex 5249	. . . . . . . . . . . . . 14 ⊢ (𝑁 ⊆ 𝑉 → 𝑁 ∈ V)
13		resfunexg 7159	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐹 ∧ 𝑁 ∈ V) → (𝐹 ↾ 𝑁) ∈ V)
14	10, 12, 13	syl2an 602	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐹 ↾ 𝑁) ∈ V)
15		f1of1 6766	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
16	15	3ad2ant1 1139	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → 𝐹:𝑉–1-1→(Vtx‘𝐻))
17		f1ores 6781	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1→(Vtx‘𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁))
18	16, 17	sylan 586	. . . . . . . . . . . . . 14 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁))
19		simpr 485	. . . . . . . . . . . . . . 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 3435	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑔 ∈ V
21	20	resex 5981	. . . . . . . . . . . . . . . . 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 6766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑔:dom (iEdg‘𝐺)–1-1→dom (iEdg‘𝐻))
24	23	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → 𝑔:dom (iEdg‘𝐺)–1-1→dom (iEdg‘𝐻))
25	24	3ad2ant2 1140	. . . . . . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . . 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 4011	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)
28		f1ores 6781	. . . . . . . . . . . . . . . . . . 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 592	. . . . . . . . . . . . . . . . . 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 29149	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐺 ∈ UHGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}))
31		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}))
32		difssd 4067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (𝒫 𝑉 ∖ {∅}) ⊆ 𝒫 𝑉)
33	31, 32	fssd 6672	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)
34	30, 33	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐺 ∈ UHGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)
35	34	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉)
36	35	anim2i 623	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶𝒫 𝑉))
37	36	3adant2 1137	. . . . . . . . . . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . . . . . . 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 1206	. . . . . . . . . . . . . . . . . . . . . . . . . 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 621	. . . . . . . . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . . . . . 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 1234	. . . . . . . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . . . . . 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 48421	. . . . . . . . . . . . . . . . . . . . . . 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 1379	. . . . . . . . . . . . . . . . . . . . . 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 6827	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑘 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝑘))
48	47	sseq1d 3946	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑘 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘𝑘) ⊆ 𝑁))
49	48	rexrab 3637	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑘 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑔‘𝑘) = 𝑗 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)(((iEdg‘𝐺)‘𝑘) ⊆ 𝑁 ∧ (𝑔‘𝑘) = 𝑗))
50	46, 49	bitr4di 290	. . . . . . . . . . . . . . . . . . . . 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 6827	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑗 → ((iEdg‘𝐻)‘𝑥) = ((iEdg‘𝐻)‘𝑗))
52	51	sseq1d 3946	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑗 → (((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁) ↔ ((iEdg‘𝐻)‘𝑗) ⊆ (𝐹 “ 𝑁)))
53	52	elrab 3629	. . . . . . . . . . . . . . . . . . . . . 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 6768	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑔 Fn dom (iEdg‘𝐺))
56	55, 27	jctir 525	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → (𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)))
57	56	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝑔 Fn dom (iEdg‘𝐺) ∧ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ⊆ dom (iEdg‘𝐺)))
58	57	3ad2ant2 1140	. . . . . . . . . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . . . . . 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 6899	. . . . . . . . . . . . . . . . . . . . . 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 312	. . . . . . . . . . . . . . . . . . . 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 2737	. . . . . . . . . . . . . . . . . . 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 6764	. . . . . . . . . . . . . . . . . 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 258	. . . . . . . . . . . . . . . . 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 3983	. . . . . . . . . . . . . . . . . . . . . . . 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 3452	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐺 ∈ UHGraph → 𝐺 ∈ V)
69	68	anim1i 621	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝐺 ∈ V ∧ 𝐻 ∈ V))
70	69	3anim3i 1160	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)))
71	70	anim1i 621	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉))
72		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 6846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} → ((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖) = (𝑔‘𝑖))
74	73	ad2antlr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6831	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 6827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 = 𝑖 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝑖))
77	76	sseq1d 3946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 = 𝑖 → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
78	77	elrab 3629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ↔ (𝑖 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁))
79	78	simprbi 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} → ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁)
80	79	ad2antlr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5968	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((iEdg‘𝐺)‘𝑖) ⊆ 𝑁 → ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))
83	72, 75, 82	3eqtr4rd 2785	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁) ∧ (𝐺 ∈ V ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) ∧ 𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) ∧ ((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))
84	83	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . 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 686	. . . . . . . . . . . . . . . . . . . . . . . 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 3151	. . . . . . . . . . . . . . . . . . . . . . 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 454	. . . . . . . . . . . . . . . . . . . . 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 1359	. . . . . . . . . . . . . . . . . . . 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 1354	. . . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . . . . 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 516	. . . . . . . . . . . . . . . 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 6755	. . . . . . . . . . . . . . . . 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 6826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (ℎ‘𝑖) = ((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))
96	95	fveq2d 6831	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → ((iEdg‘𝐻)‘(ℎ‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖)))
97	96	eqeq2d 2750	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
98	97	ralbidv 3162	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((𝑔 ↾ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})‘𝑖))))
99	94, 98	anbi12d 638	. . . . . . . . . . . . . . . 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 3536	. . . . . . . . . . . . . . 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 516	. . . . . . . . . . . . . 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 693	. . . . . . . . . . . . 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 6755	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝐹 ↾ 𝑁) → (𝑓:𝑁–1-1-onto→(𝐹 “ 𝑁) ↔ (𝐹 ↾ 𝑁):𝑁–1-1-onto→(𝐹 “ 𝑁)))
104		imaeq1 6007	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝐹 ↾ 𝑁) → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)))
105	104	eqeq1d 2741	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝐹 ↾ 𝑁) → ((𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))
106	105	ralbidv 3162	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝐹 ↾ 𝑁) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ((𝐹 ↾ 𝑁) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))))
107	106	anbi2d 636	. . . . . . . . . . . . . . 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 1928	. . . . . . . . . . . . . 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 638	. . . . . . . . . . . . 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 3536	. . . . . . . . . . . 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 1200	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V))
112		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → 𝑁 ⊆ 𝑉)
113		f1of 6767	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → 𝐹:𝑉⟶(Vtx‘𝐻))
114	113	fimassd 6676	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻))
115	114	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (𝑁 ⊆ 𝑉 → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻)))
116	115	3ad2ant1 1139	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) → (𝑁 ⊆ 𝑉 → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻)))
117	116	imp 407	. . . . . . . . . . . . 13 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐹 “ 𝑁) ⊆ (Vtx‘𝐻))
118		eqid 2739	. . . . . . . . . . . . . 14 ⊢ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}
119		eqid 2739	. . . . . . . . . . . . . 14 ⊢ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)} = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ (𝐹 “ 𝑁)}
120	4, 5, 6, 7, 118, 119	isubgrgrim 48420	. . . . . . . . . . . . 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 842	. . . . . . . . . . . 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 258	. . . . . . . . . . 11 ⊢ (((𝐹:𝑉–1-1-onto→(Vtx‘𝐻) ∧ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ V)) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁)))
123	122	3exp1 1359	. . . . . . . . . 10 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))))
124	123	exlimdv 1940	. . . . . . . . 9 ⊢ (𝐹:𝑉–1-1-onto→(Vtx‘𝐻) → (∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑔‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ V) → (𝑁 ⊆ 𝑉 → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))))
125	124	imp 407	. . . . . . . 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 416	. . . . . 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 1116	. . 3 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐻 ∈ V → (𝐺 ISubGr 𝑁) ≃_𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))))
131	130	adantld 491	. 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 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∃wex 1786 ∈ wcel 2119 ∀wral 3053 ∃wrex 3063 {crab 3391 Vcvv 3431 ∖ cdif 3880 ⊆ wss 3883 ∅c0 4261 𝒫 cpw 4529 {csn 4555 class class class wbr 5072 dom cdm 5618 ↾ cres 5620 “ cima 5621 Fun wfun 6479 Fn wfn 6480 ⟶wf 6481 –1-1→wf1 6482 –1-1-onto→wf1o 6484 ‘cfv 6485 (class class class)co 7356 Vtxcvtx 29083 iEdgciedg 29084 UHGraphcuhgr 29143 ISubGr cisubgr 48351 GraphIso cgrim 48366 ≃_𝑔𝑟 cgric 48367

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-ral 3054 df-rex 3064 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-id 5513 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-ov 7359 df-oprab 7360 df-mpo 7361 df-1st 7931 df-2nd 7932 df-1o 8395 df-map 8765 df-vtx 29085 df-iedg 29086 df-uhgr 29145 df-isubgr 48352 df-grim 48369 df-gric 48372

This theorem is referenced by: uhgrimgrlim 48478

W3C validator