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