Theorem isotrALT 3883

Description: Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. This proof is shorter than isotr 3882 in set.mm and uses fewer dummy variables, but it takes 240K vs. 207K for the web page.

Assertion

Ref	Expression
isotrALT	|- ((H Isom R, S (A, B) /\ G Isom S, T (B, C)) -> (G o. H) Isom R, T (A, C))

Proof of Theorem isotrALT

Step	Hyp	Ref	Expression
1		pm3.26 319	. . . . . 6 |- ((G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w))) -> G:B-1-1-onto->C)
2		pm3.26 319	. . . . . 6 |- ((H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))) -> H:A-1-1-onto->B)
3	1, 2	anim12i 333	. . . . 5 |- (((G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w))) /\ (H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y)))) -> (G:B-1-1-onto->C /\ H:A-1-1-onto->B))
4	3	ancoms 436	. . . 4 |- (((H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))) /\ (G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w)))) -> (G:B-1-1-onto->C /\ H:A-1-1-onto->B))
5		f1oco 3692	. . . 4 |- ((G:B-1-1-onto->C /\ H:A-1-1-onto->B) -> (G o. H):A-1-1-onto->C)
6	4, 5	syl 10	. . 3 |- (((H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))) /\ (G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w)))) -> (G o. H):A-1-1-onto->C)
7		ax-17 968	. . . . . 6 |- (H:A-1-1-onto->B -> A.x H:A-1-1-onto->B)
8		hbra1 1679	. . . . . 6 |- (A.x e. A A.y e. A (xRy <-> (H` x)S(H` y)) -> A.xA.x e. A A.y e. A (xRy <-> (H` x)S(H` y)))
9	7, 8	hban 1006	. . . . 5 |- ((H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))) -> A.x(H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))))
10		ax-17 968	. . . . 5 |- ((G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w))) -> A.x(G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w))))
11	9, 10	hban 1006	. . . 4 |- (((H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))) /\ (G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w)))) -> A.x((H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))) /\ (G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w)))))
12		ax-17 968	. . . . . . 7 |- (H:A-1-1-onto->B -> A.y H:A-1-1-onto->B)
13		ax-17 968	. . . . . . . 8 |- (x e. A -> A.y x e. A)
14		hbra1 1679	. . . . . . . 8 |- (A.y e. A (xRy <-> (H` x)S(H` y)) -> A.yA.y e. A (xRy <-> (H` x)S(H` y)))
15	13, 14	hbral 1678	. . . . . . 7 |- (A.x e. A A.y e. A (xRy <-> (H` x)S(H` y)) -> A.yA.x e. A A.y e. A (xRy <-> (H` x)S(H` y)))
16	12, 15	hban 1006	. . . . . 6 |- ((H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))) -> A.y(H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))))
17		ax-17 968	. . . . . 6 |- ((G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w))) -> A.y(G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w))))
18	16, 17	hban 1006	. . . . 5 |- (((H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))) /\ (G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w)))) -> A.y((H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))) /\ (G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w)))))
19		f1of 3674	. . . . . . . . . . 11 |- (H:A-1-1-onto->B -> H:A-->B)
20		ffvelrn 3799	. . . . . . . . . . . . 13 |- ((H:A-->B /\ x e. A) -> (H` x) e. B)
21	20	ex 373	. . . . . . . . . . . 12 |- (H:A-->B -> (x e. A -> (H` x) e. B))
22		ffvelrn 3799	. . . . . . . . . . . . 13 |- ((H:A-->B /\ y e. A) -> (H` y) e. B)
23	22	ex 373	. . . . . . . . . . . 12 |- (H:A-->B -> (y e. A -> (H` y) e. B))
24	21, 23	anim12d 556	. . . . . . . . . . 11 |- (H:A-->B -> ((x e. A /\ y e. A) -> ((H` x) e. B /\ (H` y) e. B)))
25	19, 24	syl 10	. . . . . . . . . 10 |- (H:A-1-1-onto->B -> ((x e. A /\ y e. A) -> ((H` x) e. B /\ (H` y) e. B)))
26	25	adantr 389	. . . . . . . . 9 |- ((H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))) -> ((x e. A /\ y e. A) -> ((H` x) e. B /\ (H` y) e. B)))
27		breq1 2612	. . . . . . . . . . . . 13 |- (z = (H` x) -> (zSw <-> (H` x)Sw))
28		fveq2 3709	. . . . . . . . . . . . . 14 |- (z = (H` x) -> (G` z) = (G` (H` x)))
29	28	breq1d 2619	. . . . . . . . . . . . 13 |- (z = (H` x) -> ((G` z)T(G` w) <-> (G` (H` x))T(G` w)))
30	27, 29	bibi12d 627	. . . . . . . . . . . 12 |- (z = (H` x) -> ((zSw <-> (G` z)T(G` w)) <-> ((H` x)Sw <-> (G` (H` x))T(G` w))))
31		breq2 2613	. . . . . . . . . . . . 13 |- (w = (H` y) -> ((H` x)Sw <-> (H` x)S(H` y)))
32		fveq2 3709	. . . . . . . . . . . . . 14 |- (w = (H` y) -> (G` w) = (G` (H` y)))
33	32	breq2d 2620	. . . . . . . . . . . . 13 |- (w = (H` y) -> ((G` (H` x))T(G` w) <-> (G` (H` x))T(G` (H` y))))
34	31, 33	bibi12d 627	. . . . . . . . . . . 12 |- (w = (H` y) -> (((H` x)Sw <-> (G` (H` x))T(G` w)) <-> ((H` x)S(H` y) <-> (G` (H` x))T(G` (H` y)))))
35	30, 34	rcla42v 1871	. . . . . . . . . . 11 |- (((H` x) e. B /\ (H` y) e. B) -> (A.z e. B A.w e. B (zSw <-> (G` z)T(G` w)) -> ((H` x)S(H` y) <-> (G` (H` x))T(G` (H` y)))))
36	35	com12 11	. . . . . . . . . 10 |- (A.z e. B A.w e. B (zSw <-> (G` z)T(G` w)) -> (((H` x) e. B /\ (H` y) e. B) -> ((H` x)S(H` y) <-> (G` (H` x))T(G` (H` y)))))
37	36	adantl 388	. . . . . . . . 9 |- ((G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w))) -> (((H` x) e. B /\ (H` y) e. B) -> ((H` x)S(H` y) <-> (G` (H` x))T(G` (H` y)))))
38	26, 37	sylan9 468	. . . . . . . 8 |- (((H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))) /\ (G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G