Theorem ordtrest2NEW 26351

Description: An interval-closed set A in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in RR, but in other sets like QQ there are interval-closed sets like ( pi , +oo ) i^i QQ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.)

Hypotheses

Ref	Expression
ordtNEW.b	|- B = ( Base ` K )
ordtNEW.l	|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
ordtrest2NEW.2	|- ( ph -> K e. Toset )
ordtrest2NEW.3	|- ( ph -> A C_ B )
ordtrest2NEW.4	|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. B | ( x .<_ z /\ z .<_ y ) } C_ A )

Assertion

Ref	Expression
ordtrest2NEW	|- ( ph -> (ordTop ` ( .<_ i^i ( A X. A ) ) ) = ( (ordTop ` .<_ ) ↾t A ) )

Distinct variable groups:   x, y, .<_   x, B, y   x, K, y   x, A, y, z   z, .<_   z, A   z, B   ph, x, y, z   z, K

Proof of Theorem ordtrest2NEW

Dummy variables v w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ordtrest2NEW.2	. . . 4 |- ( ph -> K e. Toset )
2		tospos 26117	. . . 4 |- ( K e. Toset -> K e. Poset )
3		posprs 15117	. . . 4 |- ( K e. Poset -> K e. Preset )
4	1, 2, 3	3syl 20	. . 3 |- ( ph -> K e. Preset )
5		ordtrest2NEW.3	. . 3 |- ( ph -> A C_ B )
6		ordtNEW.b	. . . 4 |- B = ( Base ` K )
7		ordtNEW.l	. . . 4 |- .<_ = ( ( le ` K ) i^i ( B X. B ) )
8	6, 7	ordtrestNEW 26349	. . 3 |- ( ( K e. Preset /\ A C_ B ) -> (ordTop ` ( .<_ i^i ( A X. A ) ) ) C_ ( (ordTop ` .<_ ) ↾t A ) )
9	4, 5, 8	syl2anc 661	. 2 |- ( ph -> (ordTop ` ( .<_ i^i ( A X. A ) ) ) C_ ( (ordTop ` .<_ ) ↾t A ) )
10		eqid 2441	. . . . . . . 8 |- ran ( z e. B |-> { w e. B | -. w .<_ z } ) = ran ( z e. B |-> { w e. B | -. w .<_ z } )
11		eqid 2441	. . . . . . . 8 |- ran ( z e. B |-> { w e. B | -. z .<_ w } ) = ran ( z e. B |-> { w e. B | -. z .<_ w } )
12	6, 7, 10, 11	ordtprsval 26346	. . . . . . 7 |- ( K e. Preset -> (ordTop ` .<_ ) = ( topGen ` ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ) )
13	4, 12	syl 16	. . . . . 6 |- ( ph -> (ordTop ` .<_ ) = ( topGen ` ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ) )
14	13	oveq1d 6104	. . . . 5 |- ( ph -> ( (ordTop ` .<_ ) ↾t A ) = ( ( topGen ` ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ) ↾t A ) )
15		fibas 18580	. . . . . 6 |- ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) e. TopBases
16		fvex 5699	. . . . . . . . 9 |- ( Base ` K ) e. _V
17	6, 16	eqeltri 2511	. . . . . . . 8 |- B e. _V
18	17	a1i 11	. . . . . . 7 |- ( ph -> B e. _V )
19	18, 5	ssexd 4437	. . . . . 6 |- ( ph -> A e. _V )
20		tgrest 18761	. . . . . 6 |- ( ( ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) e. TopBases /\ A e. _V ) -> ( topGen ` ( ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ↾t A ) ) = ( ( topGen ` ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ) ↾t A ) )
21	15, 19, 20	sylancr 663	. . . . 5 |- ( ph -> ( topGen ` ( ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ↾t A ) ) = ( ( topGen ` ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ) ↾t A ) )
22	14, 21	eqtr4d 2476	. . . 4 |- ( ph -> ( (ordTop ` .<_ ) ↾t A ) = ( topGen ` ( ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ↾t A ) ) )
23		firest 14369	. . . . 5 |- ( fi ` ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ↾t A ) ) = ( ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ↾t A )
24	23	fveq2i 5692	. . . 4 |- ( topGen ` ( fi ` ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ↾t A ) ) ) = ( topGen ` ( ( fi ` ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ) ↾t A ) )
25	22, 24	syl6eqr 2491	. . 3 |- ( ph -> ( (ordTop ` .<_ ) ↾t A ) = ( topGen ` ( fi ` ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ↾t A ) ) ) )
26		fvex 5699	. . . . . . . . 9 |- ( le ` K ) e. _V
27	26	inex1 4431	. . . . . . . 8 |- ( ( le ` K ) i^i ( B X. B ) ) e. _V
28	7, 27	eqeltri 2511	. . . . . . 7 |- .<_ e. _V
29	28	inex1 4431	. . . . . 6 |- ( .<_ i^i ( A X. A ) ) e. _V
30	29	a1i 11	. . . . 5 |- ( ph -> ( .<_ i^i ( A X. A ) ) e. _V )
31		ordttop 18802	. . . . 5 |- ( ( .<_ i^i ( A X. A ) ) e. _V -> (ordTop ` ( .<_ i^i ( A X. A ) ) ) e. Top )
32	30, 31	syl 16	. . . 4 |- ( ph -> (ordTop ` ( .<_ i^i ( A X. A ) ) ) e. Top )
33	6, 7, 10, 11	ordtprsuni 26347	. . . . . . . . 9 |- ( K e. Preset -> B = U. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) )
34	4, 33	syl 16	. . . . . . . 8 |- ( ph -> B = U. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) )
35	34, 18	eqeltrrd 2516	. . . . . . 7 |- ( ph -> U. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) e. _V )
36		uniexb 6384	. . . . . . 7 |- ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) e. _V <-> U. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) e. _V )
37	35, 36	sylibr 212	. . . . . 6 |- ( ph -> ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) e. _V )
38		restval 14363	. . . . . 6 |- ( ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) e. _V /\ A e. _V ) -> ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ↾t A ) = ran ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) )
39	37, 19, 38	syl2anc 661	. . . . 5 |- ( ph -> ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ↾t A ) = ran ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) )
40		dfss1 3553	. . . . . . . . . . . 12 |- ( A C_ B <-> ( B i^i A ) = A )
41	5, 40	sylib 196	. . . . . . . . . . 11 |- ( ph -> ( B i^i A ) = A )
42		eqid 2441	. . . . . . . . . . . . . . 15 |- dom ( .<_ i^i ( A X. A ) ) = dom ( .<_ i^i ( A X. A ) )
43	42	ordttopon 18795	. . . . . . . . . . . . . 14 |- ( ( .<_ i^i ( A X. A ) ) e. _V -> (ordTop ` ( .<_ i^i ( A X. A ) ) ) e. (TopOn ` dom ( .<_ i^i ( A X. A ) ) ) )
44	30, 43	syl 16	. . . . . . . . . . . . 13 |- ( ph -> (ordTop ` ( .<_ i^i ( A X. A ) ) ) e. (TopOn ` dom ( .<_ i^i ( A X. A ) ) ) )
45	6, 7	prsssdm 26345	. . . . . . . . . . . . . . 15 |- ( ( K e. Preset /\ A C_ B ) -> dom ( .<_ i^i ( A X. A ) ) = A )
46	4, 5, 45	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ph -> dom ( .<_ i^i ( A X. A ) ) = A )
47	46	fveq2d 5693	. . . . . . . . . . . . 13 |- ( ph -> (TopOn ` dom ( .<_ i^i ( A X. A ) ) ) = (TopOn ` A ) )
48	44, 47	eleqtrd 2517	. . . . . . . . . . . 12 |- ( ph -> (ordTop ` ( .<_ i^i ( A X. A ) ) ) e. (TopOn ` A ) )
49		toponmax 18531	. . . . . . . . . . . 12 |- ( (ordTop ` ( .<_ i^i ( A X. A ) ) ) e. (TopOn ` A ) -> A e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
50	48, 49	syl 16	. . . . . . . . . . 11 |- ( ph -> A e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
51	41, 50	eqeltrd 2515	. . . . . . . . . 10 |- ( ph -> ( B i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
52		elsni 3900	. . . . . . . . . . . 12 |- ( v e. { B } -> v = B )
53	52	ineq1d 3549	. . . . . . . . . . 11 |- ( v e. { B } -> ( v i^i A ) = ( B i^i A ) )
54	53	eleq1d 2507	. . . . . . . . . 10 |- ( v e. { B } -> ( ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> ( B i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
55	51, 54	syl5ibrcom 222	. . . . . . . . 9 |- ( ph -> ( v e. { B } -> ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
56	55	ralrimiv 2796	. . . . . . . 8 |- ( ph -> A. v e. { B } ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
57		ordtrest2NEW.4	. . . . . . . . . 10 |- ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. B | ( x .<_ z /\ z .<_ y ) } C_ A )
58	6, 7, 1, 5, 57	ordtrest2NEWlem 26350	. . . . . . . . 9 |- ( ph -> A. v e. ran ( z e. B |-> { w e. B | -. w .<_ z } ) ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
59		eqid 2441	. . . . . . . . . . . 12 |- (ODual ` K ) = (ODual ` K )
60	59, 6	odubas 15301	. . . . . . . . . . 11 |- B = ( Base ` (ODual ` K ) )
61	7	cnveqi 5012	. . . . . . . . . . . 12 |- `' .<_ = `' ( ( le ` K ) i^i ( B X. B ) )
62		cnvin 5242	. . . . . . . . . . . . 13 |- `' ( ( le ` K ) i^i ( B X. B ) ) = ( `' ( le ` K ) i^i `' ( B X. B ) )
63		cnvxp 5253	. . . . . . . . . . . . . 14 |- `' ( B X. B ) = ( B X. B )
64	63	ineq2i 3547	. . . . . . . . . . . . 13 |- ( `' ( le ` K ) i^i `' ( B X. B ) ) = ( `' ( le ` K ) i^i ( B X. B ) )
65		eqid 2441	. . . . . . . . . . . . . . 15 |- ( le ` K ) = ( le ` K )
66	59, 65	oduleval 15299	. . . . . . . . . . . . . 14 |- `' ( le ` K ) = ( le ` (ODual ` K ) )
67	66	ineq1i 3546	. . . . . . . . . . . . 13 |- ( `' ( le ` K ) i^i ( B X. B ) ) = ( ( le ` (ODual ` K ) ) i^i ( B X. B ) )
68	62, 64, 67	3eqtri 2465	. . . . . . . . . . . 12 |- `' ( ( le ` K ) i^i ( B X. B ) ) = ( ( le ` (ODual ` K ) ) i^i ( B X. B ) )
69	61, 68	eqtri 2461	. . . . . . . . . . 11 |- `' .<_ = ( ( le ` (ODual ` K ) ) i^i ( B X. B ) )
70	59	odutos 26122	. . . . . . . . . . . 12 |- ( K e. Toset -> (ODual ` K ) e. Toset )
71	1, 70	syl 16	. . . . . . . . . . 11 |- ( ph -> (ODual ` K ) e. Toset )
72		vex 2973	. . . . . . . . . . . . . . . . . . 19 |- y e. _V
73		vex 2973	. . . . . . . . . . . . . . . . . . 19 |- z e. _V
74	72, 73	brcnv 5020	. . . . . . . . . . . . . . . . . 18 |- ( y `' .<_ z <-> z .<_ y )
75		vex 2973	. . . . . . . . . . . . . . . . . . 19 |- x e. _V
76	73, 75	brcnv 5020	. . . . . . . . . . . . . . . . . 18 |- ( z `' .<_ x <-> x .<_ z )
77	74, 76	anbi12ci 698	. . . . . . . . . . . . . . . . 17 |- ( ( y `' .<_ z /\ z `' .<_ x ) <-> ( x .<_ z /\ z .<_ y ) )
78	77	a1i 11	. . . . . . . . . . . . . . . 16 |- ( z e. B -> ( ( y `' .<_ z /\ z `' .<_ x ) <-> ( x .<_ z /\ z .<_ y ) ) )
79	78	rabbiia 2959	. . . . . . . . . . . . . . 15 |- { z e. B | ( y `' .<_ z /\ z `' .<_ x ) } = { z e. B | ( x .<_ z /\ z .<_ y ) }
80	79	eqcomi 2445	. . . . . . . . . . . . . 14 |- { z e. B | ( x .<_ z /\ z .<_ y ) } = { z e. B | ( y `' .<_ z /\ z `' .<_ x ) }
81	80	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. B | ( x .<_ z /\ z .<_ y ) } = { z e. B | ( y `' .<_ z /\ z `' .<_ x ) } )
82	81, 57	eqsstr3d 3389	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. B | ( y `' .<_ z /\ z `' .<_ x ) } C_ A )
83	82	ancom2s 800	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. A /\ x e. A ) ) -> { z e. B | ( y `' .<_ z /\ z `' .<_ x ) } C_ A )
84	60, 69, 71, 5, 83	ordtrest2NEWlem 26350	. . . . . . . . . 10 |- ( ph -> A. v e. ran ( z e. B |-> { w e. B | -. w `' .<_ z } ) ( v i^i A ) e. (ordTop ` ( `' .<_ i^i ( A X. A ) ) ) )
85		eqidd 2442	. . . . . . . . . . . . 13 |- ( ph -> B = B )
86		vex 2973	. . . . . . . . . . . . . . . . . 18 |- w e. _V
87	86, 73	brcnv 5020	. . . . . . . . . . . . . . . . 17 |- ( w `' .<_ z <-> z .<_ w )
88	87	bicomi 202	. . . . . . . . . . . . . . . 16 |- ( z .<_ w <-> w `' .<_ z )
89	88	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> ( z .<_ w <-> w `' .<_ z ) )
90	89	notbid 294	. . . . . . . . . . . . . 14 |- ( ph -> ( -. z .<_ w <-> -. w `' .<_ z ) )
91	90	rabbidv 2962	. . . . . . . . . . . . 13 |- ( ph -> { w e. B | -. z .<_ w } = { w e. B | -. w `' .<_ z } )
92	85, 91	mpteq12dv 4368	. . . . . . . . . . . 12 |- ( ph -> ( z e. B |-> { w e. B | -. z .<_ w } ) = ( z e. B |-> { w e. B | -. w `' .<_ z } ) )
93	92	rneqd 5065	. . . . . . . . . . 11 |- ( ph -> ran ( z e. B |-> { w e. B | -. z .<_ w } ) = ran ( z e. B |-> { w e. B | -. w `' .<_ z } ) )
94		cnvin 5242	. . . . . . . . . . . . . . 15 |- `' ( .<_ i^i ( A X. A ) ) = ( `' .<_ i^i `' ( A X. A ) )
95		cnvxp 5253	. . . . . . . . . . . . . . . 16 |- `' ( A X. A ) = ( A X. A )
96	95	ineq2i 3547	. . . . . . . . . . . . . . 15 |- ( `' .<_ i^i `' ( A X. A ) ) = ( `' .<_ i^i ( A X. A ) )
97	94, 96	eqtri 2461	. . . . . . . . . . . . . 14 |- `' ( .<_ i^i ( A X. A ) ) = ( `' .<_ i^i ( A X. A ) )
98	97	fveq2i 5692	. . . . . . . . . . . . 13 |- (ordTop ` `' ( .<_ i^i ( A X. A ) ) ) = (ordTop ` ( `' .<_ i^i ( A X. A ) ) )
99	6	ressprs 26114	. . . . . . . . . . . . . . . 16 |- ( ( K e. Preset /\ A C_ B ) -> ( K ↾s A ) e. Preset )
100	4, 5, 99	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ph -> ( K ↾s A ) e. Preset )
101		eqid 2441	. . . . . . . . . . . . . . . 16 |- ( Base ` ( K ↾s A ) ) = ( Base ` ( K ↾s A ) )
102		eqid 2441	. . . . . . . . . . . . . . . 16 |- ( ( le ` ( K ↾s A ) ) i^i ( ( Base ` ( K ↾s A ) ) X. ( Base ` ( K ↾s A ) ) ) ) = ( ( le ` ( K ↾s A ) ) i^i ( ( Base ` ( K ↾s A ) ) X. ( Base ` ( K ↾s A ) ) ) )
103	101, 102	ordtcnvNEW 26348	. . . . . . . . . . . . . . 15 |- ( ( K ↾s A ) e. Preset -> (ordTop ` `' ( ( le ` ( K ↾s A ) ) i^i ( ( Base ` ( K ↾s A ) ) X. ( Base ` ( K ↾s A ) ) ) ) ) = (ordTop ` ( ( le ` ( K ↾s A ) ) i^i ( ( Base ` ( K ↾s A ) ) X. ( Base ` ( K ↾s A ) ) ) ) ) )
104	100, 103	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> (ordTop ` `' ( ( le ` ( K ↾s A ) ) i^i ( ( Base ` ( K ↾s A ) ) X. ( Base ` ( K ↾s A ) ) ) ) ) = (ordTop ` ( ( le ` ( K ↾s A ) ) i^i ( ( Base ` ( K ↾s A ) ) X. ( Base ` ( K ↾s A ) ) ) ) ) )
105	6, 7	prsss 26344	. . . . . . . . . . . . . . . . . 18 |- ( ( K e. Preset /\ A C_ B ) -> ( .<_ i^i ( A X. A ) ) = ( ( le ` K ) i^i ( A X. A ) ) )
106	4, 5, 105	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( .<_ i^i ( A X. A ) ) = ( ( le ` K ) i^i ( A X. A ) ) )
107		eqid 2441	. . . . . . . . . . . . . . . . . . . 20 |- ( K ↾s A ) = ( K ↾s A )
108	107, 65	ressle 14336	. . . . . . . . . . . . . . . . . . 19 |- ( A e. _V -> ( le ` K ) = ( le ` ( K ↾s A ) ) )
109	19, 108	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( le ` K ) = ( le ` ( K ↾s A ) ) )
110	107, 6	ressbas2 14227	. . . . . . . . . . . . . . . . . . . 20 |- ( A C_ B -> A = ( Base ` ( K ↾s A ) ) )
111	5, 110	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A = ( Base ` ( K ↾s A ) ) )
112	111, 111	xpeq12d 4863	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( A X. A ) = ( ( Base ` ( K ↾s A ) ) X. ( Base ` ( K ↾s A ) ) ) )
113	109, 112	ineq12d 3551	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( le ` K ) i^i ( A X. A ) ) = ( ( le ` ( K ↾s A ) ) i^i ( ( Base ` ( K ↾s A ) ) X. ( Base ` ( K ↾s A ) ) ) ) )
114	106, 113	eqtrd 2473	. . . . . . . . . . . . . . . 16 |- ( ph -> ( .<_ i^i ( A X. A ) ) = ( ( le ` ( K ↾s A ) ) i^i ( ( Base ` ( K ↾s A ) ) X. ( Base ` ( K ↾s A ) ) ) ) )
115	114	cnveqd 5013	. . . . . . . . . . . . . . 15 |- ( ph -> `' ( .<_ i^i ( A X. A ) ) = `' ( ( le ` ( K ↾s A ) ) i^i ( ( Base ` ( K ↾s A ) ) X. ( Base ` ( K ↾s A ) ) ) ) )
116	115	fveq2d 5693	. . . . . . . . . . . . . 14 |- ( ph -> (ordTop ` `' ( .<_ i^i ( A X. A ) ) ) = (ordTop ` `' ( ( le ` ( K ↾s A ) ) i^i ( ( Base ` ( K ↾s A ) ) X. ( Base ` ( K ↾s A ) ) ) ) ) )
117	114	fveq2d 5693	. . . . . . . . . . . . . 14 |- ( ph -> (ordTop ` ( .<_ i^i ( A X. A ) ) ) = (ordTop ` ( ( le ` ( K ↾s A ) ) i^i ( ( Base ` ( K ↾s A ) ) X. ( Base ` ( K ↾s A ) ) ) ) ) )
118	104, 116, 117	3eqtr4d 2483	. . . . . . . . . . . . 13 |- ( ph -> (ordTop ` `' ( .<_ i^i ( A X. A ) ) ) = (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
119	98, 118	syl5reqr 2488	. . . . . . . . . . . 12 |- ( ph -> (ordTop ` ( .<_ i^i ( A X. A ) ) ) = (ordTop ` ( `' .<_ i^i ( A X. A ) ) ) )
120	119	eleq2d 2508	. . . . . . . . . . 11 |- ( ph -> ( ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> ( v i^i A ) e. (ordTop ` ( `' .<_ i^i ( A X. A ) ) ) ) )
121	93, 120	raleqbidv 2929	. . . . . . . . . 10 |- ( ph -> ( A. v e. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> A. v e. ran ( z e. B |-> { w e. B | -. w `' .<_ z } ) ( v i^i A ) e. (ordTop ` ( `' .<_ i^i ( A X. A ) ) ) ) )
122	84, 121	mpbird 232	. . . . . . . . 9 |- ( ph -> A. v e. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
123		ralunb 3535	. . . . . . . . 9 |- ( A. v e. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> ( A. v e. ran ( z e. B |-> { w e. B | -. w .<_ z } ) ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) /\ A. v e. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
124	58, 122, 123	sylanbrc 664	. . . . . . . 8 |- ( ph -> A. v e. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
125		ralunb 3535	. . . . . . . 8 |- ( A. v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> ( A. v e. { B } ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) /\ A. v e. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
126	56, 124, 125	sylanbrc 664	. . . . . . 7 |- ( ph -> A. v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
127		eqid 2441	. . . . . . . 8 |- ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) = ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) )
128	127	fmpt 5862	. . . . . . 7 |- ( A. v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ( v i^i A ) e. (ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) : ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) --> (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
129	126, 128	sylib 196	. . . . . 6 |- ( ph -> ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) : ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) --> (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
130		frn 5563	. . . . . 6 |- ( ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) : ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) --> (ordTop ` ( .<_ i^i ( A X. A ) ) ) -> ran ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) C_ (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
131	129, 130	syl 16	. . . . 5 |- ( ph -> ran ( v e. ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) |-> ( v i^i A ) ) C_ (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
132	39, 131	eqsstrd 3388	. . . 4 |- ( ph -> ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ↾t A ) C_ (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
133		tgfiss 18594	. . . 4 |- ( ( (ordTop ` ( .<_ i^i ( A X. A ) ) ) e. Top /\ ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ↾t A ) C_ (ordTop ` ( .<_ i^i ( A X. A ) ) ) ) -> ( topGen ` ( fi ` ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ↾t A ) ) ) C_ (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
134	32, 132, 133	syl2anc 661	. . 3 |- ( ph -> ( topGen ` ( fi ` ( ( { B } u. ( ran ( z e. B |-> { w e. B | -. w .<_ z } ) u. ran ( z e. B |-> { w e. B | -. z .<_ w } ) ) ) ↾t A ) ) ) C_ (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
135	25, 134	eqsstrd 3388	. 2 |- ( ph -> ( (ordTop ` .<_ ) ↾t A ) C_ (ordTop ` ( .<_ i^i ( A X. A ) ) ) )
136	9, 135	eqssd 3371	1 |- ( ph -> (ordTop ` ( .<_ i^i ( A X. A ) ) ) = ( (ordTop ` .<_ ) ↾t A ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   A.wral 2713   {crab 2717   _Vcvv 2970   u. cun 3324   i^i cin 3325   C_ wss 3326   {csn 3875   U.cuni 4089   class class class wbr 4290   e. cmpt 4348   X. cxp 4836   `'ccnv 4837   dom cdm 4838   ran crn 4839   -->wf 5412   ` cfv 5416  (class class class)co 6089   ficfi 7658   Basecbs 14172   ↾_s cress 14173   lecple 14243   ↾_t crest 14357   topGenctg 14374  ordTopcordt 14435   Preset cpreset 15094   Posetcpo 15108  Tosetctos 15201  ODualcodu 15296   Topctop 18496  TopOnctopon 18497   TopBasesctb 18500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-rep 4401  ax-sep 4411  ax-nul 4419  ax-pow 4468  ax-pr 4529  ax-un 6370  ax-cnex 9336  ax-resscn 9337  ax-1cn 9338  ax-icn 9339  ax-addcl 9340  ax-addrcl 9341  ax-mulcl 9342  ax-mulrcl 9343  ax-mulcom 9344  ax-addass 9345  ax-mulass 9346  ax-distr 9347  ax-i2m1 9348  ax-1ne0 9349  ax-1rid 9350  ax-rnegex 9351  ax-rrecex 9352  ax-cnre 9353  ax-pre-lttri 9354  ax-pre-lttrn 9355  ax-pre-ltadd 9356  ax-pre-mulgt0 9357

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3185  df-csb 3287  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-pss 3342  df-nul 3636  df-if 3790  df-pw 3860  df-sn 3876  df-pr 3878  df-tp 3880  df-op 3882  df-uni 4090  df-int 4127  df-iun 4171  df-iin 4172  df-br 4291  df-opab 4349  df-mpt 4350  df-tr 4384  df-eprel 4630  df-id 4634  df-po 4639  df-so 4640  df-fr 4677  df-we 4679  df-ord 4720  df-on 4721  df-lim 4722  df-suc 4723  df-xp 4844  df-rel 4845  df-cnv 4846  df-co 4847  df-dm 4848  df-rn 4849  df-res 4850  df-ima 4851  df-iota 5379  df-fun 5418  df-fn 5419  df-f 5420  df-f1 5421  df-fo 5422  df-f1o 5423  df-fv 5424  df-riota 6050  df-ov 6092  df-oprab 6093  df-mpt2 6094  df-om 6475  df-1st 6575  df-2nd 6576  df-recs 6830  df-rdg 6864  df-1o 6918  df-oadd 6922  df-er 7099  df-en 7309  df-dom 7310  df-sdom 7311  df-fin 7312  df-fi 7659  df-pnf 9418  df-mnf 9419  df-xr 9420  df-ltxr 9421  df-le 9422  df-sub 9595  df-neg 9596  df-nn 10321  df-2 10378  df-3 10379  df-4 10380  df-5 10381  df-6 10382  df-7 10383  df-8 10384  df-9 10385  df-10 10386  df-ndx 14175  df-slot 14176  df-base 14177  df-sets 14178  df-ress 14179  df-ple 14256  df-rest 14359  df-topgen 14380  df-ordt 14437  df-preset 15096  df-poset 15114  df-toset 15202  df-odu 15297  df-top 18501  df-bases 18503  df-topon 18504

This theorem is referenced by: (None)