grimco - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > grimco		Structured version Visualization version GIF version

Theorem grimco 49202

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

**Assertion**
Ref	Expression
grimco	⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GraphIso 𝑈))

Proof of Theorem grimco Dummy variables 𝑓 𝑔 𝑖 𝑗 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2763	. . . 4 ⊢ (Vtx‘𝑇) = (Vtx‘𝑇)
2		eqid 2763	. . . 4 ⊢ (Vtx‘𝑈) = (Vtx‘𝑈)
3		eqid 2763	. . . 4 ⊢ (iEdg‘𝑇) = (iEdg‘𝑇)
4		eqid 2763	. . . 4 ⊢ (iEdg‘𝑈) = (iEdg‘𝑈)
5	1, 2, 3, 4	grimprop 49196	. . 3 ⊢ (𝐹 ∈ (𝑇 GraphIso 𝑈) → (𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ ∃𝑓(𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)))))
6		eqid 2763	. . . 4 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
7		eqid 2763	. . . 4 ⊢ (iEdg‘𝑆) = (iEdg‘𝑆)
8	6, 1, 7, 3	grimprop 49196	. . 3 ⊢ (𝐺 ∈ (𝑆 GraphIso 𝑇) → (𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦)))))
9		f1oco 6873	. . . . 5 ⊢ ((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) → (𝐹 ∘ 𝐺):(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑈))
10	9	ad2ant2r 760	. . . 4 ⊢ (((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ ∃𝑓(𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)))) ∧ (𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))))) → (𝐹 ∘ 𝐺):(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑈))
11		vex 3458	. . . . . . . . . . . . 13 ⊢ 𝑓 ∈ V
12		vex 3458	. . . . . . . . . . . . 13 ⊢ 𝑔 ∈ V
13	11, 12	coex 7969	. . . . . . . . . . . 12 ⊢ (𝑓 ∘ 𝑔) ∈ V
14	13	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ ((𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))) ∧ (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))))) → (𝑓 ∘ 𝑔) ∈ V)
15		f1oco 6873	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) → (𝑓 ∘ 𝑔):dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈))
16	15	a1d 26	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) → (∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)) → (𝑓 ∘ 𝑔):dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈)))
17	16	expcom 419	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) → (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) → (∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)) → (𝑓 ∘ 𝑔):dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈))))
18	17	impd 416	. . . . . . . . . . . . . . 15 ⊢ (𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) → ((𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))) → (𝑓 ∘ 𝑔):dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈)))
19	18	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))) → ((𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))) → (𝑓 ∘ 𝑔):dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈)))
20	19	imp 412	. . . . . . . . . . . . 13 ⊢ (((𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))) ∧ (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)))) → (𝑓 ∘ 𝑔):dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈))
21	20	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ ((𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))) ∧ (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))))) → (𝑓 ∘ 𝑔):dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈))
22		2fveq3 6916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑖 → ((iEdg‘𝑇)‘(𝑔‘𝑦)) = ((iEdg‘𝑇)‘(𝑔‘𝑖)))
23		fveq2 6911	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑖 → ((iEdg‘𝑆)‘𝑦) = ((iEdg‘𝑆)‘𝑖))
24	23	imaeq2d 6065	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑖 → (𝐺 “ ((iEdg‘𝑆)‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑖)))
25	22, 24	eqeq12d 2779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑖 → (((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦)) ↔ ((iEdg‘𝑇)‘(𝑔‘𝑖)) = (𝐺 “ ((iEdg‘𝑆)‘𝑖))))
26	25	rspcv 3576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ dom (iEdg‘𝑆) → (∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦)) → ((iEdg‘𝑇)‘(𝑔‘𝑖)) = (𝐺 “ ((iEdg‘𝑆)‘𝑖))))
27	26	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → (∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦)) → ((iEdg‘𝑇)‘(𝑔‘𝑖)) = (𝐺 “ ((iEdg‘𝑆)‘𝑖))))
28	27	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)))) → (∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦)) → ((iEdg‘𝑇)‘(𝑔‘𝑖)) = (𝐺 “ ((iEdg‘𝑆)‘𝑖))))
29		f1of 6849	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) → 𝑔:dom (iEdg‘𝑆)⟶dom (iEdg‘𝑇))
30	29	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) → 𝑔:dom (iEdg‘𝑆)⟶dom (iEdg‘𝑇))
31	30	ffvelcdmda 7111	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → (𝑔‘𝑖) ∈ dom (iEdg‘𝑇))
32	31	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ 𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈)) → (𝑔‘𝑖) ∈ dom (iEdg‘𝑇))
33		2fveq3 6916	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (𝑔‘𝑖) → ((iEdg‘𝑈)‘(𝑓‘𝑥)) = ((iEdg‘𝑈)‘(𝑓‘(𝑔‘𝑖))))
34		fveq2 6911	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑔‘𝑖) → ((iEdg‘𝑇)‘𝑥) = ((iEdg‘𝑇)‘(𝑔‘𝑖)))
35	34	imaeq2d 6065	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (𝑔‘𝑖) → (𝐹 “ ((iEdg‘𝑇)‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖))))
36	33, 35	eqeq12d 2779	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝑔‘𝑖) → (((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)) ↔ ((iEdg‘𝑈)‘(𝑓‘(𝑔‘𝑖))) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖)))))
37	36	rspcv 3576	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘𝑖) ∈ dom (iEdg‘𝑇) → (∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)) → ((iEdg‘𝑈)‘(𝑓‘(𝑔‘𝑖))) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖)))))
38	32, 37	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ 𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈)) → (∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)) → ((iEdg‘𝑈)‘(𝑓‘(𝑔‘𝑖))) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖)))))
39	30	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → 𝑔:dom (iEdg‘𝑆)⟶dom (iEdg‘𝑇))
40	39	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ 𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈)) → 𝑔:dom (iEdg‘𝑆)⟶dom (iEdg‘𝑇))
41		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → 𝑖 ∈ dom (iEdg‘𝑆))
42	41	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ 𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈)) → 𝑖 ∈ dom (iEdg‘𝑆))
43	40, 42	fvco3d 7012	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ 𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈)) → ((𝑓 ∘ 𝑔)‘𝑖) = (𝑓‘(𝑔‘𝑖)))
44	43	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ 𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈)) ∧ ((iEdg‘𝑈)‘(𝑓‘(𝑔‘𝑖))) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖)))) → ((𝑓 ∘ 𝑔)‘𝑖) = (𝑓‘(𝑔‘𝑖)))
45	44	fveq2d 6915	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ 𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈)) ∧ ((iEdg‘𝑈)‘(𝑓‘(𝑔‘𝑖))) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖)))) → ((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = ((iEdg‘𝑈)‘(𝑓‘(𝑔‘𝑖))))
46		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ 𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈)) ∧ ((iEdg‘𝑈)‘(𝑓‘(𝑔‘𝑖))) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖)))) → ((iEdg‘𝑈)‘(𝑓‘(𝑔‘𝑖))) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖))))
47	45, 46	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ 𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈)) ∧ ((iEdg‘𝑈)‘(𝑓‘(𝑔‘𝑖))) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖)))) → ((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖))))
48	47	ex 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ 𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈)) → (((iEdg‘𝑈)‘(𝑓‘(𝑔‘𝑖))) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖))) → ((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖)))))
49	38, 48	syld 48	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ 𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈)) → (∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)) → ((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖)))))
50	49	impr 460	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)))) → ((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖))))
51		imaeq2 6061	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((iEdg‘𝑇)‘(𝑔‘𝑖)) = (𝐺 “ ((iEdg‘𝑆)‘𝑖)) → (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖))) = (𝐹 “ (𝐺 “ ((iEdg‘𝑆)‘𝑖))))
52		imaco 6266	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖)) = (𝐹 “ (𝐺 “ ((iEdg‘𝑆)‘𝑖)))
53	51, 52	eqtr4di 2816	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((iEdg‘𝑇)‘(𝑔‘𝑖)) = (𝐺 “ ((iEdg‘𝑆)‘𝑖)) → (𝐹 “ ((iEdg‘𝑇)‘(𝑔‘𝑖))) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖)))
54	50, 53	sylan9eq 2818	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)))) ∧ ((iEdg‘𝑇)‘(𝑔‘𝑖)) = (𝐺 “ ((iEdg‘𝑆)‘𝑖))) → ((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖)))
55	54	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)))) → (((iEdg‘𝑇)‘(𝑔‘𝑖)) = (𝐺 “ ((iEdg‘𝑆)‘𝑖)) → ((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))
56	28, 55	syld 48	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑖 ∈ dom (iEdg‘𝑆)) ∧ (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)))) → (∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦)) → ((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))
57	56	exp31 425	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) → (𝑖 ∈ dom (iEdg‘𝑆) → ((𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))) → (∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦)) → ((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))))
58	57	com24 96	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) → (∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦)) → ((𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))) → (𝑖 ∈ dom (iEdg‘𝑆) → ((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))))
59	58	expimpd 459	. . . . . . . . . . . . . 14 ⊢ ((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) → ((𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))) → ((𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))) → (𝑖 ∈ dom (iEdg‘𝑆) → ((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))))
60	59	imp32 424	. . . . . . . . . . . . 13 ⊢ (((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ ((𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))) ∧ (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))))) → (𝑖 ∈ dom (iEdg‘𝑆) → ((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))
61	60	ralrimiv 3157	. . . . . . . . . . . 12 ⊢ (((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ ((𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))) ∧ (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))))) → ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖)))
62	21, 61	jca 521	. . . . . . . . . . 11 ⊢ (((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ ((𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))) ∧ (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))))) → ((𝑓 ∘ 𝑔):dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))
63		f1oeq1 6837	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑓 ∘ 𝑔) → (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ↔ (𝑓 ∘ 𝑔):dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈)))
64		fveq1 6910	. . . . . . . . . . . . . 14 ⊢ (𝑗 = (𝑓 ∘ 𝑔) → (𝑗‘𝑖) = ((𝑓 ∘ 𝑔)‘𝑖))
65	64	fveqeq2d 6919	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑓 ∘ 𝑔) → (((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖)) ↔ ((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))
66	65	ralbidv 3189	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑓 ∘ 𝑔) → (∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))
67	63, 66	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑓 ∘ 𝑔) → ((𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))) ↔ ((𝑓 ∘ 𝑔):dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘((𝑓 ∘ 𝑔)‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖)))))
68	14, 62, 67	spcedv 3556	. . . . . . . . . 10 ⊢ (((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ ((𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))) ∧ (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))))) → ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))
69	68	exp32 426	. . . . . . . . 9 ⊢ ((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) → ((𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))) → ((𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))) → ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))))
70	69	exlimdv 1968	. . . . . . . 8 ⊢ ((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ 𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) → (∃𝑔(𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))) → ((𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))) → ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))))
71	70	expimpd 459	. . . . . . 7 ⊢ (𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) → ((𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦)))) → ((𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))) → ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))))
72	71	com23 87	. . . . . 6 ⊢ (𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) → ((𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))) → ((𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦)))) → ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))))
73	72	exlimdv 1968	. . . . 5 ⊢ (𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) → (∃𝑓(𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥))) → ((𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦)))) → ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))))
74	73	imp31 423	. . . 4 ⊢ (((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ ∃𝑓(𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)))) ∧ (𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))))) → ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))
75	10, 74	jca 521	. . 3 ⊢ (((𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑈) ∧ ∃𝑓(𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑈)‘(𝑓‘𝑥)) = (𝐹 “ ((iEdg‘𝑇)‘𝑥)))) ∧ (𝐺:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑦 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑔‘𝑦)) = (𝐺 “ ((iEdg‘𝑆)‘𝑦))))) → ((𝐹 ∘ 𝐺):(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑈) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖)))))
76	5, 8, 75	syl2an 608	. 2 ⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → ((𝐹 ∘ 𝐺):(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑈) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖)))))
77		grimdmrel 49193	. . . . . 6 ⊢ Rel dom GraphIso
78	77	ovrcl 7487	. . . . 5 ⊢ (𝐺 ∈ (𝑆 GraphIso 𝑇) → (𝑆 ∈ V ∧ 𝑇 ∈ V))
79	78	simpld 500	. . . 4 ⊢ (𝐺 ∈ (𝑆 GraphIso 𝑇) → 𝑆 ∈ V)
80	79	adantl 487	. . 3 ⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → 𝑆 ∈ V)
81	77	ovrcl 7487	. . . . 5 ⊢ (𝐹 ∈ (𝑇 GraphIso 𝑈) → (𝑇 ∈ V ∧ 𝑈 ∈ V))
82	81	simprd 501	. . . 4 ⊢ (𝐹 ∈ (𝑇 GraphIso 𝑈) → 𝑈 ∈ V)
83	82	adantr 486	. . 3 ⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → 𝑈 ∈ V)
84		coexg 7968	. . 3 ⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ V)
85	6, 2, 7, 4	isgrim 49195	. . 3 ⊢ ((𝑆 ∈ V ∧ 𝑈 ∈ V ∧ (𝐹 ∘ 𝐺) ∈ V) → ((𝐹 ∘ 𝐺) ∈ (𝑆 GraphIso 𝑈) ↔ ((𝐹 ∘ 𝐺):(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑈) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))))
86	80, 83, 84, 85	syl3anc 1399	. 2 ⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → ((𝐹 ∘ 𝐺) ∈ (𝑆 GraphIso 𝑈) ↔ ((𝐹 ∘ 𝐺):(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑈) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑈) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑈)‘(𝑗‘𝑖)) = ((𝐹 ∘ 𝐺) “ ((iEdg‘𝑆)‘𝑖))))))
87	76, 86	mpbird 260	1 ⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GraphIso 𝑈))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∃wex 1812 ∈ wcel 2147 ∀wral 3080 Vcvv 3454 dom cdm 5656 “ cima 5659 ∘ ccom 5660 ⟶wf 6557 ⟶1-1ontowf1o 6560 ‘cfv 6561 (class class class)co 7446 Vtxcvtx 29607 iEdgciedg 29608 GraphIso cgrim 49188

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rab 3417 df-v 3456 df-sbc 3743 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-br 5107 df-opab 5172 df-id 5551 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-ov 7449 df-oprab 7450 df-mpo 7451 df-map 8880 df-grim 49191

This theorem is used by: grictr 49236

W3C validator