uhgrimisgrgric

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)

		Ref	Expression
	Hypothesis	uhgrimisgrgric.v	$⊢ V = Vtx (G)$
	Assertion	uhgrimisgrgric	$⊢ (G \in UHGraph \land F \in (G GraphIso H) \land N \subseteq V) \to (G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N])$

Proof

Step	Hyp	Ref	Expression
1		uhgrimisgrgric.v	$⊢ V = Vtx (G)$
2		grimdmrel	$⊢ Rel dom GraphIso$
3	2	ovrcl	$⊢ F \in (G GraphIso H) \to (G \in V \land H \in V)$
4	3	3ad2ant2	$⊢ (G \in UHGraph \land F \in (G GraphIso H) \land N \subseteq V) \to (G \in V \land H \in V)$
5		eqid	$⊢ Vtx (H) = Vtx (H)$
6		eqid	$⊢ iEdg (G) = iEdg (G)$
7		eqid	$⊢ iEdg (H) = iEdg (H)$
8	1 5 6 7	grimprop	$⊢ F \in (G GraphIso H) \to (F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]))$
9		f1ofun	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to Fun F$
10	9	3ad2ant1	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \to Fun F$
11	1	fvexi	$⊢ V \in V$
12	11	ssex	$⊢ N \subseteq V \to N \in V$
13		resfunexg	$⊢ (Fun F \land N \in V) \to {F ↾}_{N} \in V$
14	10 12 13	syl2an	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to {F ↾}_{N} \in V$
15		f1of1	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to F : V \underset{1-1}{⟶} Vtx (H)$
16	15	3ad2ant1	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \to F : V \underset{1-1}{⟶} Vtx (H)$
17		f1ores	$⊢ (F : V \underset{1-1}{⟶} Vtx (H) \land N \subseteq V) \to ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]$
18	16 17	sylan	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]$
19		simpr	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]$
20		vex	$⊢ g \in V$
21	20	resex	$⊢ {g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}} \in V$
22	21	a1i	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to {g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}} \in V$
23		f1of1	$⊢ g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \to g : dom iEdg (G) \underset{1-1}{⟶} dom iEdg (H)$
24	23	adantr	$⊢ (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to g : dom iEdg (G) \underset{1-1}{⟶} dom iEdg (H)$
25	24	3ad2ant2	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \to g : dom iEdg (G) \underset{1-1}{⟶} dom iEdg (H)$
26	25	ad2antrr	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to g : dom iEdg (G) \underset{1-1}{⟶} dom iEdg (H)$
27		ssrab2	$⊢ \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \subseteq dom iEdg (G)$
28		f1ores	$⊢ (g : dom iEdg (G) \underset{1-1}{⟶} dom iEdg (H) \land \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \subseteq dom iEdg (G)) \to ({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} g [\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}]$
29	26 27 28	sylancl	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to ({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} g [\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}]$
30	1 6	uhgrf	$⊢ G \in UHGraph \to iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\}$
31		id	$⊢ iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\} \to iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\}$
32		difssd	$⊢ iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\} \to 𝒫 V ∖ \{\emptyset\} \subseteq 𝒫 V$
33	31 32	fssd	$⊢ iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\} \to iEdg (G) : dom iEdg (G) ⟶ 𝒫 V$
34	30 33	syl	$⊢ G \in UHGraph \to iEdg (G) : dom iEdg (G) ⟶ 𝒫 V$
35	34	adantr	$⊢ (G \in UHGraph \land H \in V) \to iEdg (G) : dom iEdg (G) ⟶ 𝒫 V$
36	35	anim2i	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land (G \in UHGraph \land H \in V)) \to (F : V \underset{1-1 onto}{⟶} Vtx (H) \land iEdg (G) : dom iEdg (G) ⟶ 𝒫 V)$
37	36	3adant2	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \to (F : V \underset{1-1 onto}{⟶} Vtx (H) \land iEdg (G) : dom iEdg (G) ⟶ 𝒫 V)$
38	37	ad2antrr	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to (F : V \underset{1-1 onto}{⟶} Vtx (H) \land iEdg (G) : dom iEdg (G) ⟶ 𝒫 V)$
39		simp2l	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \to g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)$
40	39	anim1i	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land N \subseteq V)$
41	40	adantr	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land N \subseteq V)$
42	41	ancomd	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to (N \subseteq V \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H))$
43		simpl2r	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]$
44	43	adantr	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]$
45		uhgrimisgrgriclem	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land iEdg (G) : dom iEdg (G) ⟶ 𝒫 V) \land (N \subseteq V \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to ((j \in dom iEdg (H) \land iEdg (H) (j) \subseteq F [N]) \leftrightarrow \exists k \in dom iEdg (G) (iEdg (G) (k) \subseteq N \land g (k) = j))$
46	38 42 44 45	syl3anc	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to ((j \in dom iEdg (H) \land iEdg (H) (j) \subseteq F [N]) \leftrightarrow \exists k \in dom iEdg (G) (iEdg (G) (k) \subseteq N \land g (k) = j))$
47		fveq2	$⊢ x = k \to iEdg (G) (x) = iEdg (G) (k)$
48	47	sseq1d	$⊢ x = k \to (iEdg (G) (x) \subseteq N \leftrightarrow iEdg (G) (k) \subseteq N)$
49	48	rexrab	$⊢ \exists k \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} g (k) = j \leftrightarrow \exists k \in dom iEdg (G) (iEdg (G) (k) \subseteq N \land g (k) = j)$
50	46 49	bitr4di	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to ((j \in dom iEdg (H) \land iEdg (H) (j) \subseteq F [N]) \leftrightarrow \exists k \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} g (k) = j)$
51		fveq2	$⊢ x = j \to iEdg (H) (x) = iEdg (H) (j)$
52	51	sseq1d	$⊢ x = j \to (iEdg (H) (x) \subseteq F [N] \leftrightarrow iEdg (H) (j) \subseteq F [N])$
53	52	elrab	$⊢ j \in \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \leftrightarrow (j \in dom iEdg (H) \land iEdg (H) (j) \subseteq F [N])$
54	53	a1i	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to (j \in \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \leftrightarrow (j \in dom iEdg (H) \land iEdg (H) (j) \subseteq F [N]))$
55		f1ofn	$⊢ g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \to g Fn dom iEdg (G)$
56	55 27	jctir	$⊢ g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \to (g Fn dom iEdg (G) \land \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \subseteq dom iEdg (G))$
57	56	adantr	$⊢ (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to (g Fn dom iEdg (G) \land \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \subseteq dom iEdg (G))$
58	57	3ad2ant2	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \to (g Fn dom iEdg (G) \land \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \subseteq dom iEdg (G))$
59	58	ad2antrr	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to (g Fn dom iEdg (G) \land \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \subseteq dom iEdg (G))$
60		fvelimab	$⊢ (g Fn dom iEdg (G) \land \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \subseteq dom iEdg (G)) \to (j \in g [\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}] \leftrightarrow \exists k \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} g (k) = j)$
61	59 60	syl	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to (j \in g [\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}] \leftrightarrow \exists k \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} g (k) = j)$
62	50 54 61	3bitr4d	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to (j \in \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \leftrightarrow j \in g [\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}])$
63	62	eqrdv	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} = g [\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}]$
64	63	f1oeq3d	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \leftrightarrow ({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} g [\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}])$
65	29 64	mpbird	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to ({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\}$
66		ssralv	$⊢ \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \subseteq dom iEdg (G) \to (\forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)] \to \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} iEdg (H) (g (i)) = F [iEdg (G) (i)])$
67	27 66	ax-mp	$⊢ \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)] \to \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} iEdg (H) (g (i)) = F [iEdg (G) (i)]$
68		elex	$⊢ G \in UHGraph \to G \in V$
69	68	anim1i	$⊢ (G \in UHGraph \land H \in V) \to (G \in V \land H \in V)$
70	69	3anim3i	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in UHGraph \land H \in V)) \to (F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in V \land H \in V))$
71	70	anim1i	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in V \land H \in V)) \land N \subseteq V)$
72		simpr	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in V \land H \in V)) \land N \subseteq V) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}) \land iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to iEdg (H) (g (i)) = F [iEdg (G) (i)]$
73		fvres	$⊢ i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \to ({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i) = g (i)$
74	73	ad2antlr	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in V \land H \in V)) \land N \subseteq V) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}) \land iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to ({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i) = g (i)$
75	74	fveq2d	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in V \land H \in V)) \land N \subseteq V) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}) \land iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i)) = iEdg (H) (g (i))$
76		fveq2	$⊢ x = i \to iEdg (G) (x) = iEdg (G) (i)$
77	76	sseq1d	$⊢ x = i \to (iEdg (G) (x) \subseteq N \leftrightarrow iEdg (G) (i) \subseteq N)$
78	77	elrab	$⊢ i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \leftrightarrow (i \in dom iEdg (G) \land iEdg (G) (i) \subseteq N)$
79	78	simprbi	$⊢ i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \to iEdg (G) (i) \subseteq N$
80	79	ad2antlr	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in V \land H \in V)) \land N \subseteq V) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}) \land iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to iEdg (G) (i) \subseteq N$
81		resima2	$⊢ iEdg (G) (i) \subseteq N \to ({F ↾}_{N}) [iEdg (G) (i)] = F [iEdg (G) (i)]$
82	80 81	syl	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in V \land H \in V)) \land N \subseteq V) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}) \land iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to ({F ↾}_{N}) [iEdg (G) (i)] = F [iEdg (G) (i)]$
83	72 75 82	3eqtr4rd	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in V \land H \in V)) \land N \subseteq V) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}) \land iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i))$
84	83	ex	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in V \land H \in V)) \land N \subseteq V) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}) \to (iEdg (H) (g (i)) = F [iEdg (G) (i)] \to ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i)))$
85	71 84	sylanl1	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}) \to (iEdg (H) (g (i)) = F [iEdg (G) (i)] \to ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i)))$
86	85	ralimdva	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (\forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} iEdg (H) (g (i)) = F [iEdg (G) (i)] \to \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i)))$
87	67 86	syl5	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (\forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)] \to \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i)))$
88	87	expimpd	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to ((g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i)))$
89	88	3exp1	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to (({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \to ((G \in UHGraph \land H \in V) \to (N \subseteq V \to ((g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i))))))$
90	89	com25	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to ((g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to ((G \in UHGraph \land H \in V) \to (N \subseteq V \to (({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \to \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i))))))$
91	90	3imp1	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to (({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \to \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i)))$
92	91	imp	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i))$
93	65 92	jca	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i)))$
94		f1oeq1	$⊢ h = {g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}} \to (h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \leftrightarrow ({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\})$
95		fveq1	$⊢ h = {g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}} \to h (i) = ({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i)$
96	95	fveq2d	$⊢ h = {g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}} \to iEdg (H) (h (i)) = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i))$
97	96	eqeq2d	$⊢ h = {g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}} \to (({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (h (i)) \leftrightarrow ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i)))$
98	97	ralbidv	$⊢ h = {g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}} \to (\forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (h (i)) \leftrightarrow \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i)))$
99	94 98	anbi12d	$⊢ h = {g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}} \to ((h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (h (i))) \leftrightarrow (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (({g ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}}) (i))))$
100	22 93 99	spcedv	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to \exists h (h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (h (i)))$
101	19 100	jca	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \land ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N]) \to (({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land \exists h (h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (h (i))))$
102	18 101	mpdan	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to (({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land \exists h (h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (h (i))))$
103		f1oeq1	$⊢ f = {F ↾}_{N} \to (f : N \underset{1-1 onto}{⟶} F [N] \leftrightarrow ({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N])$
104		imaeq1	$⊢ f = {F ↾}_{N} \to f [iEdg (G) (i)] = ({F ↾}_{N}) [iEdg (G) (i)]$
105	104	eqeq1d	$⊢ f = {F ↾}_{N} \to (f [iEdg (G) (i)] = iEdg (H) (h (i)) \leftrightarrow ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (h (i)))$
106	105	ralbidv	$⊢ f = {F ↾}_{N} \to (\forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} f [iEdg (G) (i)] = iEdg (H) (h (i)) \leftrightarrow \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (h (i)))$
107	106	anbi2d	$⊢ f = {F ↾}_{N} \to ((h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} f [iEdg (G) (i)] = iEdg (H) (h (i))) \leftrightarrow (h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (h (i))))$
108	107	exbidv	$⊢ f = {F ↾}_{N} \to (\exists h (h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} f [iEdg (G) (i)] = iEdg (H) (h (i))) \leftrightarrow \exists h (h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (h (i))))$
109	103 108	anbi12d	$⊢ f = {F ↾}_{N} \to ((f : N \underset{1-1 onto}{⟶} F [N] \land \exists h (h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} f [iEdg (G) (i)] = iEdg (H) (h (i)))) \leftrightarrow (({F ↾}_{N}) : N \underset{1-1 onto}{⟶} F [N] \land \exists h (h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} ({F ↾}_{N}) [iEdg (G) (i)] = iEdg (H) (h (i)))))$
110	14 102 109	spcedv	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to \exists f (f : N \underset{1-1 onto}{⟶} F [N] \land \exists h (h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} f [iEdg (G) (i)] = iEdg (H) (h (i))))$
111		simpl3	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to (G \in UHGraph \land H \in V)$
112		simpr	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to N \subseteq V$
113		f1of	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to F : V ⟶ Vtx (H)$
114	113	fimassd	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to F [N] \subseteq Vtx (H)$
115	114	a1d	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to (N \subseteq V \to F [N] \subseteq Vtx (H))$
116	115	3ad2ant1	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \to (N \subseteq V \to F [N] \subseteq Vtx (H))$
117	116	imp	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to F [N] \subseteq Vtx (H)$
118		eqid	$⊢ \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} = \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\}$
119		eqid	$⊢ \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} = \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\}$
120	1 5 6 7 118 119	isubgrgrim	$⊢ ((G \in UHGraph \land H \in V) \land (N \subseteq V \land F [N] \subseteq Vtx (H))) \to ((G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N]) \leftrightarrow \exists f (f : N \underset{1-1 onto}{⟶} F [N] \land \exists h (h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} f [iEdg (G) (i)] = iEdg (H) (h (i)))))$
121	111 112 117 120	syl12anc	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to ((G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N]) \leftrightarrow \exists f (f : N \underset{1-1 onto}{⟶} F [N] \land \exists h (h : \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} \underset{1-1 onto}{⟶} \{x \in dom iEdg (H) \| iEdg (H) (x) \subseteq F [N]\} \land \forall i \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq N\} f [iEdg (G) (i)] = iEdg (H) (h (i)))))$
122	110 121	mpbird	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \land (G \in UHGraph \land H \in V)) \land N \subseteq V) \to (G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N])$
123	122	3exp1	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to ((g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to ((G \in UHGraph \land H \in V) \to (N \subseteq V \to (G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N]))))$
124	123	exlimdv	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to (\exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to ((G \in UHGraph \land H \in V) \to (N \subseteq V \to (G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N]))))$
125	124	imp	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \to ((G \in UHGraph \land H \in V) \to (N \subseteq V \to (G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N])))$
126	8 125	syl	$⊢ F \in (G GraphIso H) \to ((G \in UHGraph \land H \in V) \to (N \subseteq V \to (G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N])))$
127	126	expd	$⊢ F \in (G GraphIso H) \to (G \in UHGraph \to (H \in V \to (N \subseteq V \to (G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N]))))$
128	127	com12	$⊢ G \in UHGraph \to (F \in (G GraphIso H) \to (H \in V \to (N \subseteq V \to (G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N]))))$
129	128	com34	$⊢ G \in UHGraph \to (F \in (G GraphIso H) \to (N \subseteq V \to (H \in V \to (G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N]))))$
130	129	3imp	$⊢ (G \in UHGraph \land F \in (G GraphIso H) \land N \subseteq V) \to (H \in V \to (G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N]))$
131	130	adantld	$⊢ (G \in UHGraph \land F \in (G GraphIso H) \land N \subseteq V) \to ((G \in V \land H \in V) \to (G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N]))$
132	4 131	mpd	$⊢ (G \in UHGraph \land F \in (G GraphIso H) \land N \subseteq V) \to (G ISubGr N) ≃_{𝑔𝑟} (H ISubGr F [N])$

Metamath Proof Explorer

Theorem uhgrimisgrgric

Proof