grimco

Description: The composition of graph isomorphisms is a graph isomorphism. (Contributed by AV, 3-May-2025)

		Ref	Expression
	Assertion	grimco	$⊢ (F \in (T GraphIso U) \land G \in (S GraphIso T)) \to F \circ G \in (S GraphIso U)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (T) = Vtx (T)$
2		eqid	$⊢ Vtx (U) = Vtx (U)$
3		eqid	$⊢ iEdg (T) = iEdg (T)$
4		eqid	$⊢ iEdg (U) = iEdg (U)$
5	1 2 3 4	grimprop	$⊢ F \in (T GraphIso U) \to (F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land \exists f (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]))$
6		eqid	$⊢ Vtx (S) = Vtx (S)$
7		eqid	$⊢ iEdg (S) = iEdg (S)$
8	6 1 7 3	grimprop	$⊢ G \in (S GraphIso T) \to (G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists g (g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]))$
9		f1oco	$⊢ (F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \to (F \circ G) : Vtx (S) \underset{1-1 onto}{⟶} Vtx (U)$
10	9	ad2ant2r	$⊢ ((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land \exists f (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)])) \land (G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists g (g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]))) \to (F \circ G) : Vtx (S) \underset{1-1 onto}{⟶} Vtx (U)$
11		vex	$⊢ f \in V$
12		vex	$⊢ g \in V$
13	11 12	coex	$⊢ f \circ g \in V$
14	13	a1i	$⊢ ((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land ((g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]) \land (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]))) \to f \circ g \in V$
15		f1oco	$⊢ (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \to (f \circ g) : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U)$
16	15	a1d	$⊢ (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \to (\forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)] \to (f \circ g) : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U))$
17	16	expcom	$⊢ g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \to (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \to (\forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)] \to (f \circ g) : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U)))$
18	17	impd	$⊢ g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \to ((f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]) \to (f \circ g) : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U))$
19	18	adantr	$⊢ (g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]) \to ((f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]) \to (f \circ g) : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U))$
20	19	imp	$⊢ ((g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]) \land (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)])) \to (f \circ g) : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U)$
21	20	adantl	$⊢ ((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land ((g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]) \land (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]))) \to (f \circ g) : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U)$
22		2fveq3	$⊢ y = i \to iEdg (T) (g (y)) = iEdg (T) (g (i))$
23		fveq2	$⊢ y = i \to iEdg (S) (y) = iEdg (S) (i)$
24	23	imaeq2d	$⊢ y = i \to G [iEdg (S) (y)] = G [iEdg (S) (i)]$
25	22 24	eqeq12d	$⊢ y = i \to (iEdg (T) (g (y)) = G [iEdg (S) (y)] \leftrightarrow iEdg (T) (g (i)) = G [iEdg (S) (i)])$
26	25	rspcv	$⊢ i \in dom iEdg (S) \to (\forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)] \to iEdg (T) (g (i)) = G [iEdg (S) (i)])$
27	26	adantl	$⊢ (((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \to (\forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)] \to iEdg (T) (g (i)) = G [iEdg (S) (i)])$
28	27	adantr	$⊢ ((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)])) \to (\forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)] \to iEdg (T) (g (i)) = G [iEdg (S) (i)])$
29		f1of	$⊢ g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \to g : dom iEdg (S) ⟶ dom iEdg (T)$
30	29	adantl	$⊢ ((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \to g : dom iEdg (S) ⟶ dom iEdg (T)$
31	30	ffvelcdmda	$⊢ (((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \to g (i) \in dom iEdg (T)$
32	31	adantr	$⊢ ((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U)) \to g (i) \in dom iEdg (T)$
33		2fveq3	$⊢ x = g (i) \to iEdg (U) (f (x)) = iEdg (U) (f (g (i)))$
34		fveq2	$⊢ x = g (i) \to iEdg (T) (x) = iEdg (T) (g (i))$
35	34	imaeq2d	$⊢ x = g (i) \to F [iEdg (T) (x)] = F [iEdg (T) (g (i))]$
36	33 35	eqeq12d	$⊢ x = g (i) \to (iEdg (U) (f (x)) = F [iEdg (T) (x)] \leftrightarrow iEdg (U) (f (g (i))) = F [iEdg (T) (g (i))])$
37	36	rspcv	$⊢ g (i) \in dom iEdg (T) \to (\forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)] \to iEdg (U) (f (g (i))) = F [iEdg (T) (g (i))])$
38	32 37	syl	$⊢ ((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U)) \to (\forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)] \to iEdg (U) (f (g (i))) = F [iEdg (T) (g (i))])$
39	30	adantr	$⊢ (((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \to g : dom iEdg (S) ⟶ dom iEdg (T)$
40	39	adantr	$⊢ ((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U)) \to g : dom iEdg (S) ⟶ dom iEdg (T)$
41		simpr	$⊢ (((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \to i \in dom iEdg (S)$
42	41	adantr	$⊢ ((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U)) \to i \in dom iEdg (S)$
43	40 42	fvco3d	$⊢ ((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U)) \to (f \circ g) (i) = f (g (i))$
44	43	adantr	$⊢ (((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U)) \land iEdg (U) (f (g (i))) = F [iEdg (T) (g (i))]) \to (f \circ g) (i) = f (g (i))$
45	44	fveq2d	$⊢ (((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U)) \land iEdg (U) (f (g (i))) = F [iEdg (T) (g (i))]) \to iEdg (U) ((f \circ g) (i)) = iEdg (U) (f (g (i)))$
46		simpr	$⊢ (((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U)) \land iEdg (U) (f (g (i))) = F [iEdg (T) (g (i))]) \to iEdg (U) (f (g (i))) = F [iEdg (T) (g (i))]$
47	45 46	eqtrd	$⊢ (((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U)) \land iEdg (U) (f (g (i))) = F [iEdg (T) (g (i))]) \to iEdg (U) ((f \circ g) (i)) = F [iEdg (T) (g (i))]$
48	47	ex	$⊢ ((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U)) \to (iEdg (U) (f (g (i))) = F [iEdg (T) (g (i))] \to iEdg (U) ((f \circ g) (i)) = F [iEdg (T) (g (i))])$
49	38 48	syld	$⊢ ((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U)) \to (\forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)] \to iEdg (U) ((f \circ g) (i)) = F [iEdg (T) (g (i))])$
50	49	impr	$⊢ ((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)])) \to iEdg (U) ((f \circ g) (i)) = F [iEdg (T) (g (i))]$
51		imaeq2	$⊢ iEdg (T) (g (i)) = G [iEdg (S) (i)] \to F [iEdg (T) (g (i))] = F [G [iEdg (S) (i)]]$
52		imaco	$⊢ (F \circ G) [iEdg (S) (i)] = F [G [iEdg (S) (i)]]$
53	51 52	eqtr4di	$⊢ iEdg (T) (g (i)) = G [iEdg (S) (i)] \to F [iEdg (T) (g (i))] = (F \circ G) [iEdg (S) (i)]$
54	50 53	sylan9eq	$⊢ (((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)])) \land iEdg (T) (g (i)) = G [iEdg (S) (i)]) \to iEdg (U) ((f \circ g) (i)) = (F \circ G) [iEdg (S) (i)]$
55	54	ex	$⊢ ((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)])) \to (iEdg (T) (g (i)) = G [iEdg (S) (i)] \to iEdg (U) ((f \circ g) (i)) = (F \circ G) [iEdg (S) (i)])$
56	28 55	syld	$⊢ ((((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land i \in dom iEdg (S)) \land (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)])) \to (\forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)] \to iEdg (U) ((f \circ g) (i)) = (F \circ G) [iEdg (S) (i)])$
57	56	exp31	$⊢ ((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \to (i \in dom iEdg (S) \to ((f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]) \to (\forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)] \to iEdg (U) ((f \circ g) (i)) = (F \circ G) [iEdg (S) (i)])))$
58	57	com24	$⊢ ((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \to (\forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)] \to ((f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]) \to (i \in dom iEdg (S) \to iEdg (U) ((f \circ g) (i)) = (F \circ G) [iEdg (S) (i)])))$
59	58	expimpd	$⊢ (F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \to ((g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]) \to ((f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]) \to (i \in dom iEdg (S) \to iEdg (U) ((f \circ g) (i)) = (F \circ G) [iEdg (S) (i)])))$
60	59	imp32	$⊢ ((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land ((g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]) \land (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]))) \to (i \in dom iEdg (S) \to iEdg (U) ((f \circ g) (i)) = (F \circ G) [iEdg (S) (i)])$
61	60	ralrimiv	$⊢ ((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land ((g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]) \land (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]))) \to \forall i \in dom iEdg (S) iEdg (U) ((f \circ g) (i)) = (F \circ G) [iEdg (S) (i)]$
62	21 61	jca	$⊢ ((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land ((g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]) \land (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]))) \to ((f \circ g) : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) ((f \circ g) (i)) = (F \circ G) [iEdg (S) (i)])$
63		f1oeq1	$⊢ j = f \circ g \to (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \leftrightarrow (f \circ g) : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U))$
64		fveq1	$⊢ j = f \circ g \to j (i) = (f \circ g) (i)$
65	64	fveqeq2d	$⊢ j = f \circ g \to (iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)] \leftrightarrow iEdg (U) ((f \circ g) (i)) = (F \circ G) [iEdg (S) (i)])$
66	65	ralbidv	$⊢ j = f \circ g \to (\forall i \in dom iEdg (S) iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)] \leftrightarrow \forall i \in dom iEdg (S) iEdg (U) ((f \circ g) (i)) = (F \circ G) [iEdg (S) (i)])$
67	63 66	anbi12d	$⊢ j = f \circ g \to ((j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)]) \leftrightarrow ((f \circ g) : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) ((f \circ g) (i)) = (F \circ G) [iEdg (S) (i)]))$
68	14 62 67	spcedv	$⊢ ((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land ((g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]) \land (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]))) \to \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)])$
69	68	exp32	$⊢ (F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \to ((g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]) \to ((f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]) \to \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)])))$
70	69	exlimdv	$⊢ (F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \to (\exists g (g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]) \to ((f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]) \to \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)])))$
71	70	expimpd	$⊢ F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \to ((G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists g (g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)])) \to ((f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]) \to \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)])))$
72	71	com23	$⊢ F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \to ((f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]) \to ((G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists g (g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)])) \to \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)])))$
73	72	exlimdv	$⊢ F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \to (\exists f (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)]) \to ((G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists g (g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)])) \to \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)])))$
74	73	imp31	$⊢ ((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land \exists f (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)])) \land (G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists g (g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]))) \to \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)])$
75	10 74	jca	$⊢ ((F : Vtx (T) \underset{1-1 onto}{⟶} Vtx (U) \land \exists f (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall x \in dom iEdg (T) iEdg (U) (f (x)) = F [iEdg (T) (x)])) \land (G : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists g (g : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall y \in dom iEdg (S) iEdg (T) (g (y)) = G [iEdg (S) (y)]))) \to ((F \circ G) : Vtx (S) \underset{1-1 onto}{⟶} Vtx (U) \land \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)]))$
76	5 8 75	syl2an	$⊢ (F \in (T GraphIso U) \land G \in (S GraphIso T)) \to ((F \circ G) : Vtx (S) \underset{1-1 onto}{⟶} Vtx (U) \land \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)]))$
77		grimdmrel	$⊢ Rel dom GraphIso$
78	77	ovrcl	$⊢ G \in (S GraphIso T) \to (S \in V \land T \in V)$
79	78	simpld	$⊢ G \in (S GraphIso T) \to S \in V$
80	79	adantl	$⊢ (F \in (T GraphIso U) \land G \in (S GraphIso T)) \to S \in V$
81	77	ovrcl	$⊢ F \in (T GraphIso U) \to (T \in V \land U \in V)$
82	81	simprd	$⊢ F \in (T GraphIso U) \to U \in V$
83	82	adantr	$⊢ (F \in (T GraphIso U) \land G \in (S GraphIso T)) \to U \in V$
84		coexg	$⊢ (F \in (T GraphIso U) \land G \in (S GraphIso T)) \to F \circ G \in V$
85	6 2 7 4	isgrim	$⊢ (S \in V \land U \in V \land F \circ G \in V) \to (F \circ G \in (S GraphIso U) \leftrightarrow ((F \circ G) : Vtx (S) \underset{1-1 onto}{⟶} Vtx (U) \land \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)])))$
86	80 83 84 85	syl3anc	$⊢ (F \in (T GraphIso U) \land G \in (S GraphIso T)) \to (F \circ G \in (S GraphIso U) \leftrightarrow ((F \circ G) : Vtx (S) \underset{1-1 onto}{⟶} Vtx (U) \land \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (U) \land \forall i \in dom iEdg (S) iEdg (U) (j (i)) = (F \circ G) [iEdg (S) (i)])))$
87	76 86	mpbird	$⊢ (F \in (T GraphIso U) \land G \in (S GraphIso T)) \to F \circ G \in (S GraphIso U)$

Metamath Proof Explorer

Theorem grimco

Proof