Metamath Proof Explorer

Theorem ordtrest2NEWlem

Description: Lemma for ordtrest2NEW . (Contributed by Mario Carneiro, 9-Sep-2015) (Revised by Thierry Arnoux, 11-Sep-2018)

Ref Expression
Hypotheses 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 ordtrest2NEWlem 
|- ( ph -> A. v e. ran ( z e. B |-> { w e. B | -. w .<_ z } ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )

Proof

Step Hyp Ref Expression
1 ordtNEW.b 
 |-  B = ( Base ` K )
2 ordtNEW.l 
 |-  .<_ = ( ( le ` K ) i^i ( B X. B ) )
3 ordtrest2NEW.2 
 |-  ( ph -> K e. Toset )
4 ordtrest2NEW.3 
 |-  ( ph -> A C_ B )
5 ordtrest2NEW.4 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. B | ( x .<_ z /\ z .<_ y ) } C_ A )
6 inrab2 
 |-  ( { w e. B | -. w .<_ z } i^i A ) = { w e. ( B i^i A ) | -. w .<_ z }
7 sseqin2 
 |-  ( A C_ B <-> ( B i^i A ) = A )
8 4 7 sylib 
 |-  ( ph -> ( B i^i A ) = A )
9 8 adantr 
 |-  ( ( ph /\ z e. B ) -> ( B i^i A ) = A )
10 rabeq 
 |-  ( ( B i^i A ) = A -> { w e. ( B i^i A ) | -. w .<_ z } = { w e. A | -. w .<_ z } )
11 9 10 syl 
 |-  ( ( ph /\ z e. B ) -> { w e. ( B i^i A ) | -. w .<_ z } = { w e. A | -. w .<_ z } )
12 6 11 syl5eq 
 |-  ( ( ph /\ z e. B ) -> ( { w e. B | -. w .<_ z } i^i A ) = { w e. A | -. w .<_ z } )
13 fvex 
 |-  ( le ` K ) e. _V
14 13 inex1 
 |-  ( ( le ` K ) i^i ( B X. B ) ) e. _V
15 2 14 eqeltri 
 |-  .<_ e. _V
16 15 inex1 
 |-  ( .<_ i^i ( A X. A ) ) e. _V
17 16 a1i 
 |-  ( ph -> ( .<_ i^i ( A X. A ) ) e. _V )
18 eqid 
 |-  dom ( .<_ i^i ( A X. A ) ) = dom ( .<_ i^i ( A X. A ) )
19 18 ordttopon 
 |-  ( ( .<_ i^i ( A X. A ) ) e. _V -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. ( TopOn ` dom ( .<_ i^i ( A X. A ) ) ) )
20 17 19 syl 
 |-  ( ph -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. ( TopOn ` dom ( .<_ i^i ( A X. A ) ) ) )
21 tospos 
 |-  ( K e. Toset -> K e. Poset )
22 posprs 
 |-  ( K e. Poset -> K e. Proset )
23 3 21 22 3syl 
 |-  ( ph -> K e. Proset )
24 1 2 prsssdm 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom ( .<_ i^i ( A X. A ) ) = A )
25 23 4 24 syl2anc 
 |-  ( ph -> dom ( .<_ i^i ( A X. A ) ) = A )
26 25 fveq2d 
 |-  ( ph -> ( TopOn ` dom ( .<_ i^i ( A X. A ) ) ) = ( TopOn ` A ) )
27 20 26 eleqtrd 
 |-  ( ph -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. ( TopOn ` A ) )
28 toponmax 
 |-  ( ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. ( TopOn ` A ) -> A e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
29 27 28 syl 
 |-  ( ph -> A e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
30 29 adantr 
 |-  ( ( ph /\ z e. B ) -> A e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
31 rabid2 
 |-  ( A = { w e. A | -. w .<_ z } <-> A. w e. A -. w .<_ z )
32 eleq1 
 |-  ( A = { w e. A | -. w .<_ z } -> ( A e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
33 31 32 sylbir 
 |-  ( A. w e. A -. w .<_ z -> ( A e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
34 30 33 syl5ibcom 
 |-  ( ( ph /\ z e. B ) -> ( A. w e. A -. w .<_ z -> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
35 dfrex2 
 |-  ( E. w e. A w .<_ z <-> -. A. w e. A -. w .<_ z )
36 breq1 
 |-  ( w = x -> ( w .<_ z <-> x .<_ z ) )
37 36 cbvrexvw 
 |-  ( E. w e. A w .<_ z <-> E. x e. A x .<_ z )
38 35 37 bitr3i 
 |-  ( -. A. w e. A -. w .<_ z <-> E. x e. A x .<_ z )
39 ordttop 
 |-  ( ( .<_ i^i ( A X. A ) ) e. _V -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. Top )
40 17 39 syl 
 |-  ( ph -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. Top )
41 40 adantr 
 |-  ( ( ph /\ z e. B ) -> ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. Top )
42 0opn 
 |-  ( ( ordTop ` ( .<_ i^i ( A X. A ) ) ) e. Top -> (/) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
43 41 42 syl 
 |-  ( ( ph /\ z e. B ) -> (/) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
44 43 adantr 
 |-  ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) -> (/) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
45 eleq1 
 |-  ( { w e. A | -. w .<_ z } = (/) -> ( { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> (/) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
46 44 45 syl5ibrcom 
 |-  ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) -> ( { w e. A | -. w .<_ z } = (/) -> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
47 rabn0 
 |-  ( { w e. A | -. w .<_ z } =/= (/) <-> E. w e. A -. w .<_ z )
48 breq1 
 |-  ( w = y -> ( w .<_ z <-> y .<_ z ) )
49 48 notbid 
 |-  ( w = y -> ( -. w .<_ z <-> -. y .<_ z ) )
50 49 cbvrexvw 
 |-  ( E. w e. A -. w .<_ z <-> E. y e. A -. y .<_ z )
51 47 50 bitri 
 |-  ( { w e. A | -. w .<_ z } =/= (/) <-> E. y e. A -. y .<_ z )
52 3 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) /\ y e. A ) -> K e. Toset )
53 4 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) -> A C_ B )
54 53 sselda 
 |-  ( ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) /\ y e. A ) -> y e. B )
55 simpllr 
 |-  ( ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) /\ y e. A ) -> z e. B )
56 1 2 trleile 
 |-  ( ( K e. Toset /\ y e. B /\ z e. B ) -> ( y .<_ z \/ z .<_ y ) )
57 52 54 55 56 syl3anc 
 |-  ( ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) /\ y e. A ) -> ( y .<_ z \/ z .<_ y ) )
58 57 ord 
 |-  ( ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) /\ y e. A ) -> ( -. y .<_ z -> z .<_ y ) )
59 an4 
 |-  ( ( ( x e. A /\ x .<_ z ) /\ ( y e. A /\ z .<_ y ) ) <-> ( ( x e. A /\ y e. A ) /\ ( x .<_ z /\ z .<_ y ) ) )
60 rabss 
 |-  ( { z e. B | ( x .<_ z /\ z .<_ y ) } C_ A <-> A. z e. B ( ( x .<_ z /\ z .<_ y ) -> z e. A ) )
61 5 60 sylib 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> A. z e. B ( ( x .<_ z /\ z .<_ y ) -> z e. A ) )
62 61 r19.21bi 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ z e. B ) -> ( ( x .<_ z /\ z .<_ y ) -> z e. A ) )
63 62 an32s 
 |-  ( ( ( ph /\ z e. B ) /\ ( x e. A /\ y e. A ) ) -> ( ( x .<_ z /\ z .<_ y ) -> z e. A ) )
64 63 impr 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( x e. A /\ y e. A ) /\ ( x .<_ z /\ z .<_ y ) ) ) -> z e. A )
65 59 64 sylan2b 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( x e. A /\ x .<_ z ) /\ ( y e. A /\ z .<_ y ) ) ) -> z e. A )
66 brinxp 
 |-  ( ( w e. A /\ z e. A ) -> ( w .<_ z <-> w ( .<_ i^i ( A X. A ) ) z ) )
67 66 ancoms 
 |-  ( ( z e. A /\ w e. A ) -> ( w .<_ z <-> w ( .<_ i^i ( A X. A ) ) z ) )
68 67 notbid 
 |-  ( ( z e. A /\ w e. A ) -> ( -. w .<_ z <-> -. w ( .<_ i^i ( A X. A ) ) z ) )
69 68 rabbidva 
 |-  ( z e. A -> { w e. A | -. w .<_ z } = { w e. A | -. w ( .<_ i^i ( A X. A ) ) z } )
70 65 69 syl 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( x e. A /\ x .<_ z ) /\ ( y e. A /\ z .<_ y ) ) ) -> { w e. A | -. w .<_ z } = { w e. A | -. w ( .<_ i^i ( A X. A ) ) z } )
71 25 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( x e. A /\ x .<_ z ) /\ ( y e. A /\ z .<_ y ) ) ) -> dom ( .<_ i^i ( A X. A ) ) = A )
72 rabeq 
 |-  ( dom ( .<_ i^i ( A X. A ) ) = A -> { w e. dom ( .<_ i^i ( A X. A ) ) | -. w ( .<_ i^i ( A X. A ) ) z } = { w e. A | -. w ( .<_ i^i ( A X. A ) ) z } )
73 71 72 syl 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( x e. A /\ x .<_ z ) /\ ( y e. A /\ z .<_ y ) ) ) -> { w e. dom ( .<_ i^i ( A X. A ) ) | -. w ( .<_ i^i ( A X. A ) ) z } = { w e. A | -. w ( .<_ i^i ( A X. A ) ) z } )
74 70 73 eqtr4d 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( x e. A /\ x .<_ z ) /\ ( y e. A /\ z .<_ y ) ) ) -> { w e. A | -. w .<_ z } = { w e. dom ( .<_ i^i ( A X. A ) ) | -. w ( .<_ i^i ( A X. A ) ) z } )
75 16 a1i 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( x e. A /\ x .<_ z ) /\ ( y e. A /\ z .<_ y ) ) ) -> ( .<_ i^i ( A X. A ) ) e. _V )
76 65 71 eleqtrrd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( x e. A /\ x .<_ z ) /\ ( y e. A /\ z .<_ y ) ) ) -> z e. dom ( .<_ i^i ( A X. A ) ) )
77 18 ordtopn1 
 |-  ( ( ( .<_ i^i ( A X. A ) ) e. _V /\ z e. dom ( .<_ i^i ( A X. A ) ) ) -> { w e. dom ( .<_ i^i ( A X. A ) ) | -. w ( .<_ i^i ( A X. A ) ) z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
78 75 76 77 syl2anc 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( x e. A /\ x .<_ z ) /\ ( y e. A /\ z .<_ y ) ) ) -> { w e. dom ( .<_ i^i ( A X. A ) ) | -. w ( .<_ i^i ( A X. A ) ) z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
79 74 78 eqeltrd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( x e. A /\ x .<_ z ) /\ ( y e. A /\ z .<_ y ) ) ) -> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
80 79 anassrs 
 |-  ( ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) /\ ( y e. A /\ z .<_ y ) ) -> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
81 80 expr 
 |-  ( ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) /\ y e. A ) -> ( z .<_ y -> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
82 58 81 syld 
 |-  ( ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) /\ y e. A ) -> ( -. y .<_ z -> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
83 82 rexlimdva 
 |-  ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) -> ( E. y e. A -. y .<_ z -> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
84 51 83 syl5bi 
 |-  ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) -> ( { w e. A | -. w .<_ z } =/= (/) -> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
85 46 84 pm2.61dne 
 |-  ( ( ( ph /\ z e. B ) /\ ( x e. A /\ x .<_ z ) ) -> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
86 85 rexlimdvaa 
 |-  ( ( ph /\ z e. B ) -> ( E. x e. A x .<_ z -> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
87 38 86 syl5bi 
 |-  ( ( ph /\ z e. B ) -> ( -. A. w e. A -. w .<_ z -> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
88 34 87 pm2.61d 
 |-  ( ( ph /\ z e. B ) -> { w e. A | -. w .<_ z } e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
89 12 88 eqeltrd 
 |-  ( ( ph /\ z e. B ) -> ( { w e. B | -. w .<_ z } i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
90 89 ralrimiva 
 |-  ( ph -> A. z e. B ( { w e. B | -. w .<_ z } i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )
91 fvex 
 |-  ( Base ` K ) e. _V
92 1 91 eqeltri 
 |-  B e. _V
93 92 a1i 
 |-  ( ph -> B e. _V )
94 rabexg 
 |-  ( B e. _V -> { w e. B | -. w .<_ z } e. _V )
95 93 94 syl 
 |-  ( ph -> { w e. B | -. w .<_ z } e. _V )
96 95 ralrimivw 
 |-  ( ph -> A. z e. B { w e. B | -. w .<_ z } e. _V )
97 eqid 
 |-  ( z e. B |-> { w e. B | -. w .<_ z } ) = ( z e. B |-> { w e. B | -. w .<_ z } )
98 ineq1 
 |-  ( v = { w e. B | -. w .<_ z } -> ( v i^i A ) = ( { w e. B | -. w .<_ z } i^i A ) )
99 98 eleq1d 
 |-  ( v = { w e. B | -. w .<_ z } -> ( ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> ( { w e. B | -. w .<_ z } i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
100 97 99 ralrnmptw 
 |-  ( A. z e. B { w e. B | -. w .<_ z } e. _V -> ( A. v e. ran ( z e. B |-> { w e. B | -. w .<_ z } ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> A. z e. B ( { w e. B | -. w .<_ z } i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
101 96 100 syl 
 |-  ( ph -> ( A. v e. ran ( z e. B |-> { w e. B | -. w .<_ z } ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) <-> A. z e. B ( { w e. B | -. w .<_ z } i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) ) )
102 90 101 mpbird 
 |-  ( ph -> A. v e. ran ( z e. B |-> { w e. B | -. w .<_ z } ) ( v i^i A ) e. ( ordTop ` ( .<_ i^i ( A X. A ) ) ) )