Theorem isoini 3885

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 3878	. . . . . . . . 9 |- (H Isom R, S (A, B) -> H:A-1-1-onto->B)
2		f1ofo 3680	. . . . . . . . 9 |- (H:A-1-1-onto->B -> H:A-onto->B)
3		forn 3659	. . . . . . . . . 10 |- (H:A-onto->B -> ran H = B)
4	3	eleq2d 1533	. . . . . . . . 9 |- (H:A-onto->B -> (y e. ran H <-> y e. B))
5	1, 2, 4	3syl 20	. . . . . . . 8 |- (H Isom R, S (A, B) -> (y e. ran H <-> y e. B))
6		f1ofn 3675	. . . . . . . . 9 |- (H:A-1-1-onto->B -> H Fn A)
7		fvelrnb 3745	. . . . . . . . 9 |- (H Fn A -> (y e. ran H <-> E.x e. A (H` x) = y))
8	1, 6, 7	3syl 20	. . . . . . . 8 |- (H Isom R, S (A, B) -> (y e. ran H <-> E.x e. A (H` x) = y))
9	5, 8	bitr3d 528	. . . . . . 7 |- (H Isom R, S (A, B) -> (y e. B <-> E.x e. A (H` x) = y))
10		fvex 3717	. . . . . . . . 9 |- (H` D) e. V
11		visset 1804	. . . . . . . . . 10 |- y e. V
12	11	eliniseg 3413	. . . . . . . . 9 |- ((H` D) e. V -> (y e. (`'S"{(H` D)}) <-> yS(H` D)))
13	10, 12	ax-mp 7	. . . . . . . 8 |- (y e. (`'S"{(H` D)}) <-> yS(H` D))
14	13	a1i 8	. . . . . . 7 |- (H Isom R, S (A, B) -> (y e. (`'S"{(H` D)}) <-> yS(H` D)))
15	9, 14	anbi12d 626	. . . . . 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 389	. . . . 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 1804	. . . . . . . . . . . . . 14 |- x e. V
18	17	eliniseg 3413	. . . . . . . . . . . . 13 |- (D e. A -> (x e. (`'R"{D}) <-> xRD))
19	18	anbi2d 614	. . . . . . . . . . . 12 |- (D e. A -> ((x e. A /\ x e. (`'R"{D})) <-> (x e. A /\ xRD)))
20		elin 2197	. . . . . . . . . . . 12 |- (x e. (A i^i (`'R"{D})) <-> (x e. A /\ x e. (`'R"{D})))
21	19, 20	syl5bb 530	. . . . . . . . . . 11 |- (D e. A -> (x e. (A i^i (`'R"{D})) <-> (x e. A /\ xRD)))
22	21	anbi1d 615	. . . . . . . . . 10 |- (D e. A -> ((x e. (A i^i (`'R"{D})) /\ xHy) <-> ((x e. A /\ xRD) /\ xHy)))
23		anass 439	. . . . . . . . . 10 |- (((x e. A /\ xRD) /\ xHy) <-> (x e. A /\ (xRD /\ xHy)))
24	22, 23	syl6bb 534	. . . . . . . . 9 |- (D e. A -> ((x e. (A i^i (`'R"{D})) /\ xHy) <-> (x e. A /\ (xRD /\ xHy))))
25	24	adantl 388	. . . . . . . 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 3879	. . . . . . . . . . . . . 14 |- ((H Isom R, S (A, B) /\ (x e. A /\ D e. A)) -> (xRD <-> (H` x)S(H` D)))
27	11	fnbrfvb 3738	. . . . . . . . . . . . . . . . 17 |- ((H Fn A /\ x e. A) -> ((H` x) = y <-> xHy))
28	27	bicomd 519	. . . . . . . . . . . . . . . 16 |- ((H Fn A /\ x e. A) -> (xHy <-> (H` x) = y))
29	1, 6	syl 10	. . . . . . . . . . . . . . . 16 |- (H Isom R, S (A, B) -> H Fn A)
30	28, 29	sylan 448	. . . . . . . . . . . . . . 15 |- ((H Isom R, S (A, B) /\ x e. A) -> (xHy <-> (H` x) = y))
31	30	adantrr 395	. . . . . . . . . . . . . 14 |- ((H Isom R, S (A, B) /\ (x e. A /\ D e. A)) -> (xHy <-> (H` x) = y))
32	26, 31	anbi12d 626	. . . . . . . . . . . . 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 435	. . . . . . . . . . . . . 14 |- (((H` x)S(H` D) /\ (H` x) = y) <-> ((H` x) = y /\ (H` x)S(H` D)))
34		breq1 2612	. . . . . . . . . . . . . . 15 |- ((H` x) = y -> ((H` x)S(H` D) <-> yS(H` D)))
35	34	pm5.32i 643	. . . . . . . . . . . . . 14 |- (((H` x) = y /\ (H` x)S(H` D)) <-> ((H` x) = y /\ yS(H` D)))
36	33, 35	bitr 173	. . . . . . . . . . . . 13 |- (((H` x)S(H` D) /\ (H` x) = y) <-> ((H` x) = y /\ yS(H` D)))
37	32, 36	syl6bb 534	. . . . . . . . . . . 12 |- ((H Isom R, S (A, B) /\ (x e. A /\ D e. A)) -> ((xRD /\ xHy) <-> ((H` x) = y /\ yS(H` D))))
38	37	exp32 377	. . . . . . . . . . 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 350	. . . . . . . . 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 645	. . . . . . . 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 526	. . . . . . 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	rexbidv2 1658	. . . . . 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 1755	. . . . . 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 534	. . . . 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 529	. . . 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 2197	. . . 4 |- (y e. (B i^i (`'S"{(H` D)})) <-> (y e. B /\ y e. (`'S"{(H` D)})))
48	46, 47	syl5bb 530	. . 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	abbi2dv 1570	. 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 3389	. 2 |- (H"(A i^i (`'R"{D}))) = {y | E.x e. (A i^i (`'R"{D}))xHy}
51	49, 50	syl6reqr 1518	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 3   <-> wb 146   /\ wa 223   = wceq&nb