Theorem isotrALT 4875

Description: Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. This proof is shorter than isotr 4874 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		simpl 346	. . . . . 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		simpl 346	. . . . . 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 360	. . . . 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 484	. . . 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 4661	. . . 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 12	. . 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 1317	. . . . . 6 |- (H:A-1-1-onto->B -> A.x H:A-1-1-onto->B)
8		hbra1 2147	. . . . . 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 1356	. . . . 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 1317	. . . . 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 1356	. . . 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 1317	. . . . . . 7 |- (H:A-1-1-onto->B -> A.y H:A-1-1-onto->B)
13		ax-17 1317	. . . . . . . 8 |- (x e. A -> A.y x e. A)
14		hbra1 2147	. . . . . . . 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 2146	. . . . . . 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 1356	. . . . . 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 1317	. . . . . 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 1356	. . . . 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 4635	. . . . . . . . . . 11 |- (H:A-1-1-onto->B -> H:A-->B)
20		ffvelrn 4787	. . . . . . . . . . . . 13 |- ((H:A-->B /\ x e. A) -> (H` x) e. B)
21	20	ex 402	. . . . . . . . . . . 12 |- (H:A-->B -> (x e. A -> (H` x) e. B))
22		ffvelrn 4787	. . . . . . . . . . . . 13 |- ((H:A-->B /\ y e. A) -> (H` y) e. B)
23	22	ex 402	. . . . . . . . . . . 12 |- (H:A-->B -> (y e. A -> (H` y) e. B))
24	21, 23	anim12d 617	. . . . . . . . . . 11 |- (H:A-->B -> ((x e. A /\ y e. A) -> ((H` x) e. B /\ (H` y) e. B)))
25	19, 24	syl 12	. . . . . . . . . 10 |- (H:A-1-1-onto->B -> ((x e. A /\ y e. A) -> ((H` x) e. B /\ (H` y) e. B)))
26	25	adantr 425	. . . . . . . . 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 3341	. . . . . . . . . . . . 13 |- (z = (H` x) -> (zSw <-> (H` x)Sw))
28		fveq2 4681	. . . . . . . . . . . . . 14 |- (z = (H` x) -> (G` z) = (G` (H` x)))
29	28	breq1d 3348	. . . . . . . . . . . . 13 |- (z = (H` x) -> ((G` z)T(G` w) <-> (G` (H` x))T(G` w)))
30	27, 29	bibi12d 691	. . . . . . . . . . . 12 |- (z = (H` x) -> ((zSw <-> (G` z)T(G` w)) <-> ((H` x)Sw <-> (G` (H` x))T(G` w))))
31		breq2 3342	. . . . . . . . . . . . 13 |- (w = (H` y) -> ((H` x)Sw <-> (H` x)S(H` y)))
32		fveq2 4681	. . . . . . . . . . . . . 14 |- (w = (H` y) -> (G` w) = (G` (H` y)))
33	32	breq2d 3350	. . . . . . . . . . . . 13 |- (w = (H` y) -> ((G` (H` x))T(G` w) <-> (G` (H` x))T(G` (H` y))))
34	31, 33	bibi12d 691	. . . . . . . . . . . 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 2384	. . . . . . . . . . 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 14	. . . . . . . . . 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 424	. . . . . . . . 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 517	. . . . . . . 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` w)))) -> ((x e. A /\ y e. A) -> ((H` x)S(H` y) <-> (G` (H` x))T(G` (H` y)))))
39	38	imp 377	. . . . . . 7 |- ((((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)))) /\ (x e. A /\ y e. A)) -> ((H` x)S(H` y) <-> (G` (H` x))T(G` (H` y))))
40		ra42 2157	. . . . . . . . . 10 |- (A.x e. A A.y e. A (xRy <-> (H` x)S(H` y)) -> ((x e. A /\ y e. A) -> (xRy <-> (H` x)S(H` y))))
41	40	imp 377	. . . . . . . . 9 |- ((A.x e. A A.y e. A (xRy <-> (H` x)S(H` y)) /\ (x e. A /\ y e. A)) -> (xRy <-> (H` x)S(H` y)))
42	41	adantll 428	. . . . . . . 8 |- (((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)) -> (xRy <-> (H` x)S(H` y)))
43	42	adantlr 429	. . . . . . 7 |- ((((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)))) /\ (x e. A /\ y e. A)) -> (xRy <-> (H` x)S(H` y)))
44		fvco3 4739	. . . . . . . . . . . 12 |- ((Fun G /\ H:A-->B /\ x e. A) -> ((G o. H)` x) = (G` (H` x)))
45	44	3expa 1067	. . . . . . . . . . 11 |- (((Fun G /\ H:A-->B) /\ x e. A) -> ((G o. H)` x) = (G` (H` x)))
46		fvco3 4739	. . . . . . . . . . . 12 |- ((Fun G /\ H:A-->B /\ y e. A) -> ((G o. H)` y) = (G` (H` y)))
47	46	3expa 1067	. . . . . . . . . . 11 |- (((Fun G /\ H:A-->B) /\ y e. A) -> ((G o. H)` y) = (G` (H` y)))
48	45, 47	breqan12d 3354	. . . . . . . . . 10 |- ((((Fun G /\ H:A-->B) /\ x e. A) /\ ((Fun G /\ H:A-->B) /\ y e. A)) -> (((G o. H)` x)T((G o. H)` y) <-> (G` (H` x))T(G` (H` y))))
49	48	anandis 570	. . . . . . . . 9 |- (((Fun G /\ H:A-->B) /\ (x e. A /\ y e. A)) -> (((G o. H)` x)T((G o. H)` y) <-> (G` (H` x))T(G` (H` y))))
50		f1ofun 4637	. . . . . . . . . 10 |- (G:B-1-1-onto->C -> Fun G)
51	50, 19	anim12i 360	. . . . . . . . 9 |- ((G:B-1-1-onto->C /\ H:A-1-1-onto->B) -> (Fun G /\ H:A-->B))
52	49, 51	sylan 497	. . . . . . . 8 |- (((G:B-1-1-onto->C /\ H:A-1-1-onto->B) /\ (x e. A /\ y e. A)) -> (((G o. H)` x)T((G o. H)` y) <-> (G` (H` x))T(G` (H` y))))
53	52, 4	sylan 497	. . . . . . 7 |- ((((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)))) /\ (x e. A /\ y e. A)) -> (((G o. H)` x)T((G o. H)` y) <-> (G` (H` x))T(G` (H` y))))
54	39, 43, 53	3bitr4d 609	. . . . . 6 |- ((((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)))) /\ (x e. A /\ y e. A)) -> (xRy <-> ((G o. H)` x)T((G o. H)` y)))
55	54	exp32 408	. . . . 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)))) -> (x e. A -> (y e. A -> (xRy <-> ((G o. H)` x)T((G o. H)` y)))))
56	18, 13, 55	r19.21ad 2180	. . . 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)))) -> (x e. A -> A.y e. A (xRy <-> ((G o. H)` x)T((G o. H)` y))))
57	11, 56	r19.21ai 2174	. . 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)))) -> A.x e. A A.y e. A (xRy <-> ((G o. H)` x)T((G o. H)` y)))
58	6, 57	jca 310	. 2 |- (((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 /\ A.x e. A A.y e. A (xRy <-> ((G o. H)` x)T((G o. H)` y))))
59		df-iso 4015	. . 3 |- (H Isom R, S (A, B) <-> (H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))))
60		df-iso 4015	. . 3 |- (G Isom S, T (B, C) <-> (G:B-1-1-onto->C /\ A.z e. B A.w e. B (zSw <-> (G` z)T(G` w))))
61	59, 60	anbi12i 540	. 2 |- ((H Isom R, S (A, B) /\ G Isom S, T (B, C)) <-> ((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)))))
62		df-iso 4015	. 2 |- ((G o. H) Isom R, T (A, C) <-> ((G o. H):A-1-1-onto->C /\ A.x e. A A.y e. A (xRy <-> ((G o. H)` x)T((G o. H)` y))))
63	58, 61, 62	3imtr4i 236	1 |- ((H Isom R, S (A, B) /\ G Isom S, T (B, C)) -> (G o. H) Isom R, T (A, C))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  A.wral 2105   class class class wbr 3338   o. ccom 3990  Fun wfun 3992  -->wf 3994  -1-1-onto->wf1o 3997  ` cfv 3998   Isom wiso 3999

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-iso 4015

Copyright terms: Public domain