Metamath Proof Explorer

Theorem supsrlem

Description: Lemma for supremum theorem. (Contributed by NM, 21-May-1996) (Revised by Mario Carneiro, 15-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypotheses supsrlem.1 
|- B = { w | ( C +R [ <. w , 1P >. ] ~R ) e. A }
supsrlem.2 
|- C e. R.
Assertion supsrlem 
|- ( ( C e. A /\ E. x e. R. A. y e. A y  E. x e. R. ( A. y e. A -. x  E. z e. A y

Proof

Step Hyp Ref Expression
1 supsrlem.1 
 |-  B = { w | ( C +R [ <. w , 1P >. ] ~R ) e. A }
2 supsrlem.2 
 |-  C e. R.
3 0idsr 
 |-  ( C e. R. -> ( C +R 0R ) = C )
4 2 3 mp1i 
 |-  ( ( C e. A /\ E. x e. R. A. y e. A y  ( C +R 0R ) = C )
5 simpl 
 |-  ( ( C e. A /\ E. x e. R. A. y e. A y  C e. A )
6 4 5 eqeltrd 
 |-  ( ( C e. A /\ E. x e. R. A. y e. A y  ( C +R 0R ) e. A )
7 1pr 
 |-  1P e. P.
8 7 elexi 
 |-  1P e. _V
9 opeq1 
 |-  ( w = 1P -> <. w , 1P >. = <. 1P , 1P >. )
10 9 eceq1d 
 |-  ( w = 1P -> [ <. w , 1P >. ] ~R = [ <. 1P , 1P >. ] ~R )
11 df-0r 
 |-  0R = [ <. 1P , 1P >. ] ~R
12 10 11 eqtr4di 
 |-  ( w = 1P -> [ <. w , 1P >. ] ~R = 0R )
13 12 oveq2d 
 |-  ( w = 1P -> ( C +R [ <. w , 1P >. ] ~R ) = ( C +R 0R ) )
14 13 eleq1d 
 |-  ( w = 1P -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A <-> ( C +R 0R ) e. A ) )
15 8 14 1 elab2 
 |-  ( 1P e. B <-> ( C +R 0R ) e. A )
16 6 15 sylibr 
 |-  ( ( C e. A /\ E. x e. R. A. y e. A y  1P e. B )
17 16 ne0d 
 |-  ( ( C e. A /\ E. x e. R. A. y e. A y  B =/= (/) )
18 breq1 
 |-  ( y = C -> ( y  C
19 18 rspccv 
 |-  ( A. y e. A y  ( C e. A -> C
20 0lt1sr 
 |-  0R
21 m1r 
 |-  -1R e. R.
22 ltasr 
 |-  ( -1R e. R. -> ( 0R  ( -1R +R 0R )
23 21 22 ax-mp 
 |-  ( 0R  ( -1R +R 0R )
24 20 23 mpbi 
 |-  ( -1R +R 0R )
25 0idsr 
 |-  ( -1R e. R. -> ( -1R +R 0R ) = -1R )
26 21 25 ax-mp 
 |-  ( -1R +R 0R ) = -1R
27 m1p1sr 
 |-  ( -1R +R 1R ) = 0R
28 24 26 27 3brtr3i 
 |-  -1R
29 ltasr 
 |-  ( C e. R. -> ( -1R  ( C +R -1R )
30 2 29 ax-mp 
 |-  ( -1R  ( C +R -1R )
31 28 30 mpbi 
 |-  ( C +R -1R )
32 2 3 ax-mp 
 |-  ( C +R 0R ) = C
33 31 32 breqtri 
 |-  ( C +R -1R )
34 ltsosr 
 |-
35 ltrelsr 
 |-
36 34 35 sotri 
 |-  ( ( ( C +R -1R )  ( C +R -1R )
37 33 36 mpan 
 |-  ( C  ( C +R -1R )
38 2 map2psrpr 
 |-  ( ( C +R -1R )  E. v e. P. ( C +R [ <. v , 1P >. ] ~R ) = x )
39 37 38 sylib 
 |-  ( C  E. v e. P. ( C +R [ <. v , 1P >. ] ~R ) = x )
40 19 39 syl6 
 |-  ( A. y e. A y  ( C e. A -> E. v e. P. ( C +R [ <. v , 1P >. ] ~R ) = x ) )
41 breq2 
 |-  ( ( C +R [ <. v , 1P >. ] ~R ) = x -> ( y . ] ~R ) <-> y
42 41 ralbidv 
 |-  ( ( C +R [ <. v , 1P >. ] ~R ) = x -> ( A. y e. A y . ] ~R ) <-> A. y e. A y
43 1 abeq2i 
 |-  ( w e. B <-> ( C +R [ <. w , 1P >. ] ~R ) e. A )
44 breq1 
 |-  ( y = ( C +R [ <. w , 1P >. ] ~R ) -> ( y . ] ~R ) <-> ( C +R [ <. w , 1P >. ] ~R ) . ] ~R ) ) )
45 44 rspccv 
 |-  ( A. y e. A y . ] ~R ) -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A -> ( C +R [ <. w , 1P >. ] ~R ) . ] ~R ) ) )
46 2 ltpsrpr 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) . ] ~R ) <-> w
47 45 46 syl6ib 
 |-  ( A. y e. A y . ] ~R ) -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A -> w
48 43 47 syl5bi 
 |-  ( A. y e. A y . ] ~R ) -> ( w e. B -> w
49 48 ralrimiv 
 |-  ( A. y e. A y . ] ~R ) -> A. w e. B w
50 42 49 syl6bir 
 |-  ( ( C +R [ <. v , 1P >. ] ~R ) = x -> ( A. y e. A y  A. w e. B w
51 50 com12 
 |-  ( A. y e. A y  ( ( C +R [ <. v , 1P >. ] ~R ) = x -> A. w e. B w
52 51 reximdv 
 |-  ( A. y e. A y  ( E. v e. P. ( C +R [ <. v , 1P >. ] ~R ) = x -> E. v e. P. A. w e. B w
53 40 52 syld 
 |-  ( A. y e. A y  ( C e. A -> E. v e. P. A. w e. B w
54 53 rexlimivw 
 |-  ( E. x e. R. A. y e. A y  ( C e. A -> E. v e. P. A. w e. B w
55 54 impcom 
 |-  ( ( C e. A /\ E. x e. R. A. y e. A y  E. v e. P. A. w e. B w
56 supexpr 
 |-  ( ( B =/= (/) /\ E. v e. P. A. w e. B w 
 E. v e. P. ( A. w e. B -. v 
 E. u e. B w
57 17 55 56 syl2anc 
 |-  ( ( C e. A /\ E. x e. R. A. y e. A y  E. v e. P. ( A. w e. B -. v 
 E. u e. B w
58 2 mappsrpr 
 |-  ( ( C +R -1R ) . ] ~R ) <-> v e. P. )
59 35 brel 
 |-  ( ( C +R -1R ) . ] ~R ) -> ( ( C +R -1R ) e. R. /\ ( C +R [ <. v , 1P >. ] ~R ) e. R. ) )
60 58 59 sylbir 
 |-  ( v e. P. -> ( ( C +R -1R ) e. R. /\ ( C +R [ <. v , 1P >. ] ~R ) e. R. ) )
61 60 simprd 
 |-  ( v e. P. -> ( C +R [ <. v , 1P >. ] ~R ) e. R. )
62 61 adantl 
 |-  ( ( ( C e. A /\ E. x e. R. A. y e. A y  ( C +R [ <. v , 1P >. ] ~R ) e. R. )
63 34 35 sotri 
 |-  ( ( ( C +R -1R ) . ] ~R ) /\ ( C +R [ <. v , 1P >. ] ~R )  ( C +R -1R )
64 58 63 sylanbr 
 |-  ( ( v e. P. /\ ( C +R [ <. v , 1P >. ] ~R )  ( C +R -1R )
65 2 map2psrpr 
 |-  ( ( C +R -1R )  E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y )
66 64 65 sylib 
 |-  ( ( v e. P. /\ ( C +R [ <. v , 1P >. ] ~R )  E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y )
67 rexex 
 |-  ( E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y -> E. w ( C +R [ <. w , 1P >. ] ~R ) = y )
68 df-ral 
 |-  ( A. w e. B -. v 
 A. w ( w e. B -> -. v
69 19.29 
 |-  ( ( A. w ( w e. B -> -. v 
. ] ~R ) = y ) -> E. w ( ( w e. B -> -. v 
. ] ~R ) = y ) )
70 eleq1 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A <-> y e. A ) )
71 43 70 syl5bb 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( w e. B <-> y e. A ) )
72 2 ltpsrpr 
 |-  ( ( C +R [ <. v , 1P >. ] ~R ) . ] ~R ) <-> v
73 breq2 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( ( C +R [ <. v , 1P >. ] ~R ) . ] ~R ) <-> ( C +R [ <. v , 1P >. ] ~R )
74 72 73 bitr3id 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( v 
 ( C +R [ <. v , 1P >. ] ~R )
75 74 notbid 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( -. v 
 -. ( C +R [ <. v , 1P >. ] ~R )
76 71 75 imbi12d 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( ( w e. B -> -. v 
 ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R )
77 76 biimpac 
 |-  ( ( ( w e. B -> -. v 
. ] ~R ) = y ) -> ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R )
78 77 exlimiv 
 |-  ( E. w ( ( w e. B -> -. v 
. ] ~R ) = y ) -> ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R )
79 69 78 syl 
 |-  ( ( A. w ( w e. B -> -. v 
. ] ~R ) = y ) -> ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R )
80 68 79 sylanb 
 |-  ( ( A. w e. B -. v 
. ] ~R ) = y ) -> ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R )
81 80 expcom 
 |-  ( E. w ( C +R [ <. w , 1P >. ] ~R ) = y -> ( A. w e. B -. v 
 ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R )
82 66 67 81 3syl 
 |-  ( ( v e. P. /\ ( C +R [ <. v , 1P >. ] ~R )  ( A. w e. B -. v 
 ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R )
83 82 impd 
 |-  ( ( v e. P. /\ ( C +R [ <. v , 1P >. ] ~R )  ( ( A. w e. B -. v 
 -. ( C +R [ <. v , 1P >. ] ~R )
84 83 impancom 
 |-  ( ( v e. P. /\ ( A. w e. B -. v 
 ( ( C +R [ <. v , 1P >. ] ~R )  -. ( C +R [ <. v , 1P >. ] ~R )
85 84 pm2.01d 
 |-  ( ( v e. P. /\ ( A. w e. B -. v 
 -. ( C +R [ <. v , 1P >. ] ~R )
86 85 expr 
 |-  ( ( v e. P. /\ A. w e. B -. v 
 ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R )
87 86 ralrimiv 
 |-  ( ( v e. P. /\ A. w e. B -. v 
 A. y e. A -. ( C +R [ <. v , 1P >. ] ~R )
88 87 ex 
 |-  ( v e. P. -> ( A. w e. B -. v 
 A. y e. A -. ( C +R [ <. v , 1P >. ] ~R )
89 88 adantl 
 |-  ( ( ( C e. A /\ E. x e. R. A. y e. A y  ( A. w e. B -. v 
 A. y e. A -. ( C +R [ <. v , 1P >. ] ~R )
90 r19.29 
 |-  ( ( A. w e. P. ( w 
 E. u e. B w 
. ] ~R ) = y ) -> E. w e. P. ( ( w 
 E. u e. B w 
. ] ~R ) = y ) )
91 breq1 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( ( C +R [ <. w , 1P >. ] ~R ) . ] ~R ) <-> y . ] ~R ) ) )
92 46 91 bitr3id 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( w 
 y . ] ~R ) ) )
93 92 biimprd 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( y . ] ~R ) -> w
94 vex 
 |-  u e. _V
95 opeq1 
 |-  ( w = u -> <. w , 1P >. = <. u , 1P >. )
96 95 eceq1d 
 |-  ( w = u -> [ <. w , 1P >. ] ~R = [ <. u , 1P >. ] ~R )
97 96 oveq2d 
 |-  ( w = u -> ( C +R [ <. w , 1P >. ] ~R ) = ( C +R [ <. u , 1P >. ] ~R ) )
98 97 eleq1d 
 |-  ( w = u -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A <-> ( C +R [ <. u , 1P >. ] ~R ) e. A ) )
99 94 98 1 elab2 
 |-  ( u e. B <-> ( C +R [ <. u , 1P >. ] ~R ) e. A )
100 breq2 
 |-  ( z = ( C +R [ <. u , 1P >. ] ~R ) -> ( ( C +R [ <. w , 1P >. ] ~R )  ( C +R [ <. w , 1P >. ] ~R ) . ] ~R ) ) )
101 2 ltpsrpr 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) . ] ~R ) <-> w
102 100 101 bitrdi 
 |-  ( z = ( C +R [ <. u , 1P >. ] ~R ) -> ( ( C +R [ <. w , 1P >. ] ~R )  w
103 102 rspcev 
 |-  ( ( ( C +R [ <. u , 1P >. ] ~R ) e. A /\ w 
 E. z e. A ( C +R [ <. w , 1P >. ] ~R )
104 99 103 sylanb 
 |-  ( ( u e. B /\ w 
 E. z e. A ( C +R [ <. w , 1P >. ] ~R )
105 104 rexlimiva 
 |-  ( E. u e. B w 
 E. z e. A ( C +R [ <. w , 1P >. ] ~R )
106 breq1 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( ( C +R [ <. w , 1P >. ] ~R )  y
107 106 rexbidv 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( E. z e. A ( C +R [ <. w , 1P >. ] ~R )  E. z e. A y
108 105 107 syl5ib 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( E. u e. B w 
 E. z e. A y
109 93 108 imim12d 
 |-  ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( ( w 
 E. u e. B w 
 ( y . ] ~R ) -> E. z e. A y
110 109 impcom 
 |-  ( ( ( w 
 E. u e. B w 
. ] ~R ) = y ) -> ( y . ] ~R ) -> E. z e. A y
111 110 rexlimivw 
 |-  ( E. w e. P. ( ( w 
 E. u e. B w 
. ] ~R ) = y ) -> ( y . ] ~R ) -> E. z e. A y
112 90 111 syl 
 |-  ( ( A. w e. P. ( w 
 E. u e. B w 
. ] ~R ) = y ) -> ( y . ] ~R ) -> E. z e. A y
113 65 112 sylan2b 
 |-  ( ( A. w e. P. ( w 
 E. u e. B w 
 ( y . ] ~R ) -> E. z e. A y
114 113 ex 
 |-  ( A. w e. P. ( w 
 E. u e. B w 
 ( ( C +R -1R )  ( y . ] ~R ) -> E. z e. A y
115 114 adantl 
 |-  ( ( ( C e. A /\ v e. P. ) /\ A. w e. P. ( w 
 E. u e. B w 
 ( ( C +R -1R )  ( y . ] ~R ) -> E. z e. A y
116 115 a1dd 
 |-  ( ( ( C e. A /\ v e. P. ) /\ A. w e. P. ( w 
 E. u e. B w 
 ( ( C +R -1R )  ( y e. R. -> ( y . ] ~R ) -> E. z e. A y
117 34 35 sotri2 
 |-  ( ( y e. R. /\ -. ( C +R -1R )  y
118 33 117 mp3an3 
 |-  ( ( y e. R. /\ -. ( C +R -1R )  y
119 breq2 
 |-  ( z = C -> ( y  y
120 119 rspcev 
 |-  ( ( C e. A /\ y  E. z e. A y
121 120 ex 
 |-  ( C e. A -> ( y  E. z e. A y
122 121 a1dd 
 |-  ( C e. A -> ( y  ( y . ] ~R ) -> E. z e. A y
123 118 122 syl5 
 |-  ( C e. A -> ( ( y e. R. /\ -. ( C +R -1R )  ( y . ] ~R ) -> E. z e. A y
124 123 expcomd 
 |-  ( C e. A -> ( -. ( C +R -1R )  ( y e. R. -> ( y . ] ~R ) -> E. z e. A y
125 124 ad2antrr 
 |-  ( ( ( C e. A /\ v e. P. ) /\ A. w e. P. ( w 
 E. u e. B w 
 ( -. ( C +R -1R )  ( y e. R. -> ( y . ] ~R ) -> E. z e. A y
126 116 125 pm2.61d 
 |-  ( ( ( C e. A /\ v e. P. ) /\ A. w e. P. ( w 
 E. u e. B w 
 ( y e. R. -> ( y . ] ~R ) -> E. z e. A y
127 126 ralrimiv 
 |-  ( ( ( C e. A /\ v e. P. ) /\ A. w e. P. ( w 
 E. u e. B w 
 A. y e. R. ( y . ] ~R ) -> E. z e. A y
128 127 ex 
 |-  ( ( C e. A /\ v e. P. ) -> ( A. w e. P. ( w 
 E. u e. B w 
 A. y e. R. ( y . ] ~R ) -> E. z e. A y
129 128 adantlr 
 |-  ( ( ( C e. A /\ E. x e. R. A. y e. A y  ( A. w e. P. ( w 
 E. u e. B w 
 A. y e. R. ( y . ] ~R ) -> E. z e. A y
130 89 129 anim12d 
 |-  ( ( ( C e. A /\ E. x e. R. A. y e. A y  ( ( A. w e. B -. v 
 E. u e. B w 
 ( A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) . ] ~R ) -> E. z e. A y
131 breq1 
 |-  ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( x  ( C +R [ <. v , 1P >. ] ~R )
132 131 notbid 
 |-  ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( -. x  -. ( C +R [ <. v , 1P >. ] ~R )
133 132 ralbidv 
 |-  ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( A. y e. A -. x  A. y e. A -. ( C +R [ <. v , 1P >. ] ~R )
134 breq2 
 |-  ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( y  y . ] ~R ) ) )
135 134 imbi1d 
 |-  ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( ( y  E. z e. A y  ( y . ] ~R ) -> E. z e. A y
136 135 ralbidv 
 |-  ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( A. y e. R. ( y  E. z e. A y  A. y e. R. ( y . ] ~R ) -> E. z e. A y
137 133 136 anbi12d 
 |-  ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( ( A. y e. A -. x  E. z e. A y  ( A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) . ] ~R ) -> E. z e. A y
138 137 rspcev 
 |-  ( ( ( C +R [ <. v , 1P >. ] ~R ) e. R. /\ ( A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) . ] ~R ) -> E. z e. A y  E. x e. R. ( A. y e. A -. x  E. z e. A y
139 62 130 138 syl6an 
 |-  ( ( ( C e. A /\ E. x e. R. A. y e. A y  ( ( A. w e. B -. v 
 E. u e. B w 
 E. x e. R. ( A. y e. A -. x  E. z e. A y
140 139 rexlimdva 
 |-  ( ( C e. A /\ E. x e. R. A. y e. A y  ( E. v e. P. ( A. w e. B -. v 
 E. u e. B w 
 E. x e. R. ( A. y e. A -. x  E. z e. A y
141 57 140 mpd 
 |-  ( ( C e. A /\ E. x e. R. A. y e. A y  E. x e. R. ( A. y e. A -. x  E. z e. A y