Theorem isoini 2938

Description: Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33.

Assertion

Ref	Expression
isoini	|- ((H Isom R, S (A, B) /\ D e. A) -> (H"(A i^i (`'R"{D}))) = (B i^i (`'S"{(H` D)})))

Proof of Theorem isoini

Step	Hyp	Ref	Expression
1		isof1o 2931	. . . . . . . . 9 |- (H Isom R, S (A, B) -> H:A-1-1-onto->B)
2		f1ofo 2806	. . . . . . . . 9 |- (H:A-1-1-onto->B -> H:A-onto->B)
3		forn 2789	. . . . . . . . . 10 |- (H:A-onto->B -> ran H = B)
4	3	eleq2d 1156	. . . . . . . . 9 |- (H:A-onto->B -> (y e. ran H <-> y e. B))
5	1, 2, 4	3syl 21	. . . . . . . 8 |- (H Isom R, S (A, B) -> (y e. ran H <-> y e. B))
6		f1ofn 2801	. . . . . . . . 9 |- (H:A-1-1-onto->B -> H Fn A)
7		fvelrn 2883	. . . . . . . . 9 |- (H Fn A -> (y e. ran H <-> E.x e. A (H` x) = y))
8	1, 6, 7	3syl 21	. . . . . . . 8 |- (H Isom R, S (A, B) -> (y e. ran H <-> E.x e. A (H` x) = y))
9	5, 8	bitr3d 408	. . . . . . 7 |- (H Isom R, S (A, B) -> (y e. B <-> E.x e. A (H` x) = y))
10		fvex 2838	. . . . . . . . 9 |- (H` D) e. V
11		visset 1350	. . . . . . . . . 10 |- y e. V
12	11	eliniseg 2618	. . . . . . . . 9 |- ((H` D) e. V -> (y e. (`'S"{(H` D)}) <-> yS(H` D)))
13	10, 12	ax-mp 6	. . . . . . . 8 |- (y e. (`'S"{(H` D)}) <-> yS(H` D))
14	13	a1i 7	. . . . . . 7 |- (H Isom R, S (A, B) -> (y e. (`'S"{(H` D)}) <-> yS(H` D)))
15	9, 14	anbi12d 476	. . . . . 6 |- (H Isom R, S (A, B) -> ((y e. B /\ y e. (`'S"{(H` D)})) <-> (E.x e. A (H` x) = y /\ yS(H` D))))
16	15	adantr 306	. . . . 5 |- ((H Isom R, S (A, B) /\ D e. A) -> ((y e. B /\ y e. (`'S"{(H` D)})) <-> (E.x e. A (H` x) = y /\ yS(H` D))))
17		visset 1350	. . . . . . . . . . . . . 14 |- x e. V
18	17	eliniseg 2618	. . . . . . . . . . . . 13 |- (D e. A -> (x e. (`'R"{D}) <-> xRD))
19	18	anbi2d 468	. . . . . . . . . . . 12 |- (D e. A -> ((x e. A /\ x e. (`'R"{D})) <-> (x e. A /\ xRD)))
20		elin 1635	. . . . . . . . . . . 12 |- (x e. (A i^i (`'R"{D})) <-> (x e. A /\ x e. (`'R"{D})))
21	19, 20	syl5bb 410	. . . . . . . . . . 11 |- (D e. A -> (x e. (A i^i (`'R"{D})) <-> (x e. A /\ xRD)))
22	21	anbi1d 469	. . . . . . . . . 10 |- (D e. A -> ((x e. (A i^i (`'R"{D})) /\ xHy) <-> ((x e. A /\ xRD) /\ xHy)))
23		anass 336	. . . . . . . . . 10 |- (((x e. A /\ xRD) /\ xHy) <-> (x e. A /\ (xRD /\ xHy)))
24	22, 23	syl6bb 414	. . . . . . . . 9 |- (D e. A -> ((x e. (A i^i (`'R"{D})) /\ xHy) <-> (x e. A /\ (xRD /\ xHy))))
25	24	adantl 305	. . . . . . . 8 |- ((H Isom R, S (A, B) /\ D e. A) -> ((x e. (A i^i (`'R"{D})) /\ xHy) <-> (x e. A /\ (xRD /\ xHy))))
26		isorel 2932	. . . . . . . . . . . . . 14 |- ((H Isom R, S (A, B) /\ (x e. A /\ D e. A)) -> (xRD <-> (H` x)S(H` D)))
27	11	fnfvbr 2855	. . . . . . . . . . . . . . . . 17 |- ((H Fn A /\ x e. A) -> ((H` x) = y <-> xHy))
28	27	bicomd 399	. . . . . . . . . . . . . . . 16 |- ((H Fn A /\ x e. A) -> (xHy <-> (H` x) = y))
29	1, 6	syl 12	. . . . . . . . . . . . . . . 16 |- (H Isom R, S (A, B) -> H Fn A)
30	28, 29	sylan 343	. . . . . . . . . . . . . . 15 |- ((H Isom R, S (A, B) /\ x e. A) -> (xHy <-> (H` x) = y))
31	30	adantrr 312	. . . . . . . . . . . . . 14 |- ((H Isom R, S (A, B) /\ (x e. A /\ D e. A)) -> (xHy <-> (H` x) = y))
32	26, 31	anbi12d 476	. . . . . . . . . . . . 13 |- ((H Isom R, S (A, B) /\ (x e. A /\ D e. A)) -> ((xRD /\ xHy) <-> ((H` x)S(H` D) /\ (H` x) = y)))
33		ancom 333	. . . . . . . . . . . . . 14 |- (((H` x)S(H` D) /\ (H` x) = y) <-> ((H` x) = y /\ (H` x)S(H` D)))
34		breq1 2065	. . . . . . . . . . . . . . 15 |- ((H` x) = y -> ((H` x)S(H` D) <-> yS(H` D)))
35	34	pm5.32i 489	. . . . . . . . . . . . . 14 |- (((H` x) = y /\ (H` x)S(H` D)) <-> ((H` x) = y /\ yS(H` D)))
36	33, 35	bitr 151	. . . . . . . . . . . . 13 |- (((H` x)S(H` D) /\ (H` x) = y) <-> ((H` x) = y /\ yS(H` D)))
37	32, 36	syl6bb 414	. . . . . . . . . . . 12 |- ((H Isom R, S (A, B) /\ (x e. A /\ D e. A)) -> ((xRD /\ xHy) <-> ((H` x) = y /\ yS(H` D))))
38	37	exp32 294	. . . . . . . . . . 11 |- (H Isom R, S (A, B) -> (x e. A -> (D e. A -> ((xRD /\ xHy) <-> ((H` x) = y /\ yS(H` D))))))
39	38	com23 32	. . . . . . . . . 10 |- (H Isom R, S (A, B) -> (D e. A -> (x e. A -> ((xRD /\ xHy) <-> ((H` x) = y /\ yS(H` D))))))
40	39	imp 277	. . . . . . . . 9 |- ((H Isom R, S (A, B) /\ D e. A) -> (x e. A -> ((xRD /\ xHy) <-> ((H` x) = y /\ yS(H` D)))))
41	40	pm5.32d 491	. . . . . . . 8 |- ((H Isom R, S (A, B) /\ D e. A) -> ((x e. A /\ (xRD /\ xHy)) <-> (x e. A /\ ((H` x) = y /\ yS(H` D)))))
42	25, 41	bitrd 406	. . . . . . 7 |- ((H Isom R, S (A, B) /\ D e. A) -> ((x e. (A i^i (`'R"{D})) /\ xHy) <-> (x e. A /\ ((H` x) = y /\ yS(H` D)))))
43	42	birexdv2 1222	. . . . . 6 |- ((H Isom R, S (A, B) /\ D e. A) -> (E.x e. (A i^i (`'R"{D}))xHy <-> E.x e. A ((H` x) = y /\ yS(H` D))))
44		r19.41v 1302	. . . . . 6 |- (E.x e. A ((H` x) = y /\ yS(H` D)) <-> (E.x e. A (H` x) = y /\ yS(H` D)))
45	43, 44	syl6bb 414	. . . . 5 |- ((H Isom R, S (A, B) /\ D e. A) -> (E.x e. (A i^i (`'R"{D}))xHy <-> (E.x e. A (H` x) = y /\ yS(H` D))))
46	16, 45	bitr4d 409	. . . 4 |- ((H Isom R, S (A, B) /\ D e. A) -> ((y e. B /\ y e. (`'S"{(H` D)})) <-> E.x e. (A i^i (`'R"{D}))xHy))
47		elin 1635	. . . 4 |- (y e. (B i^i (`'S"{(H` D)})) <-> (y e. B /\ y e. (`'S"{(H` D)})))
48	46, 47	syl5bb 410	. . 3 |- ((H Isom R, S (A, B) /\ D e. A) -> (y e. (B i^i (`'S"{(H` D)})) <-> E.x e. (A i^i (`'R"{D}))xHy))
49	48	biabrdv 1184	. 2 |- ((H Isom R, S (A, B) /\ D e. A) -> (B i^i (`'S"{(H` D)})) = {y | E.x e. (A i^i (`'R"{D}))xHy})
50		dfima2 2604	. 2 |- (H"(A i^i (`'R"{D}))) = {y | E.x e. (A i^i (`'R"{D}))xHy}
51	49, 50	syl6reqr 1143	1 |- ((H Isom R, S (A, B) /\ D e. A) -> (H"(A i^i (`'R"{D}))) = (B i^i (`'S"{(H` D)})))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196  {cab 1090   = wceq 1091   e. wcel 1092  E.wrex 1202  Vcvv 1348   i^i cin 1486  {csn 1808   class class class wbr 2054  `'ccnv 2409  ran crn 2411  "cima 2413   Fn wfn 2417  -onto->wfo 2420  -1-1-onto->wf1o 2421  ` cfv 2422   Isom wiso 2423

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11&nb