ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  suplocsrlem Unicode version
Theorem suplocsrlem 8175
Description: Lemma for suplocsr 8176. The set A has a least upper bound. (Contributed by Jim Kingdon, 16-Jan-2024.)
Hypotheses
Ref Expression
suplocsrlem.b |- B = { w e. P. | ( C +R [ <. w , 1P >. ] ~R ) e. A }
suplocsrlem.ss |- ( ph -> A C_ R. )
suplocsrlem.c |- ( ph -> C e. A )
suplocsrlem.ub |- ( ph -> E. x e. R. A. y e. A y <R x )
suplocsrlem.loc |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )
Assertion
Ref Expression
suplocsrlem |- ( ph -> E. x e. R. ( A. y e. A -. x <R y /\ A. y e. R. ( y <R x -> E. z e. A y <R z ) ) )
Distinct variable groups:   w, A, x, y, z   w, B, y, z, x   w, C, y, z, x   ph, w, y, x, z
Proof of Theorem suplocsrlem
Dummy variables b u v a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 suplocsrlem.b . . 3 |- B = { w e. P. | ( C +R [ <. w , 1P >. ] ~R ) e. A }
2 suplocsrlem.ss . . 3 |- ( ph -> A C_ R. )
3 suplocsrlem.c . . 3 |- ( ph -> C e. A )
4 suplocsrlem.ub . . 3 |- ( ph -> E. x e. R. A. y e. A y <R x )
5 suplocsrlem.loc . . 3 |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )
61, 2, 3, 4, 5suplocsrlempr 8174 . 2 |- ( ph -> E. v e. P. ( A. w e. B -. v <P w /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) )
7 simpr 110 . . . . . . 7 |- ( ( ph /\ v e. P. ) -> v e. P. )
82, 3sseldd 3249 . . . . . . . 8 |- ( ph -> C e. R. )
98adantr 276 . . . . . . 7 |- ( ( ph /\ v e. P. ) -> C e. R. )
10 mappsrprg 8171 . . . . . . 7 |- ( ( v e. P. /\ C e. R. ) -> ( C +R -1R ) <R ( C +R [ <. v , 1P >. ] ~R ) )
117, 9, 10syl2anc 415 . . . . . 6 |- ( ( ph /\ v e. P. ) -> ( C +R -1R ) <R ( C +R [ <. v , 1P >. ] ~R ) )
12 ltrelsr 8105 . . . . . . 7 |- <R C_ ( R. X. R. )
1312brel 4827 . . . . . 6 |- ( ( C +R -1R ) <R ( C +R [ <. v , 1P >. ] ~R ) -> ( ( C +R -1R ) e. R. /\ ( C +R [ <. v , 1P >. ] ~R ) e. R. ) )
1411, 13syl 14 . . . . 5 |- ( ( ph /\ v e. P. ) -> ( ( C +R -1R ) e. R. /\ ( C +R [ <. v , 1P >. ] ~R ) e. R. ) )
1514simprd 114 . . . 4 |- ( ( ph /\ v e. P. ) -> ( C +R [ <. v , 1P >. ] ~R ) e. R. )
16 breq2 4134 . . . . . . . 8 |- ( w = a -> ( v <P w <-> v <P a ) )
1716notbid 677 . . . . . . 7 |- ( w = a -> ( -. v <P w <-> -. v <P a ) )
1817cbvralv 2786 . . . . . 6 |- ( A. w e. B -. v <P w <-> A. a e. B -. v <P a )
19 ltsosr 8131 . . . . . . . . . . . . . . 15 |- <R Or R.
2019, 12sotri 5183 . . . . . . . . . . . . . 14 |- ( ( ( C +R -1R ) <R ( C +R [ <. v , 1P >. ] ~R ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> ( C +R -1R ) <R y )
2111, 20sylan 283 . . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. P. ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> ( C +R -1R ) <R y )
229adantr 276 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. P. ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> C e. R. )
23 map2psrprg 8172 . . . . . . . . . . . . . 14 |- ( C e. R. -> ( ( C +R -1R ) <R y <-> E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y ) )
2422, 23syl 14 . . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. P. ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> ( ( C +R -1R ) <R y <-> E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y ) )
2521, 24mpbid 147 . . . . . . . . . . . 12 |- ( ( ( ph /\ v e. P. ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y )
2625adantlr 481 . . . . . . . . . . 11 |- ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y )
2726adantlr 481 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y )
28 simplr 533 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> ( C +R [ <. v , 1P >. ] ~R ) <R y )
29 simprr 537 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> ( C +R [ <. w , 1P >. ] ~R ) = y )
3028, 29breqtrrd 4158 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> ( C +R [ <. v , 1P >. ] ~R ) <R ( C +R [ <. w , 1P >. ] ~R ) )
317ad4antr 498 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> v e. P. )
32 simprl 535 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> w e. P. )
339ad4antr 498 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> C e. R. )
34 ltpsrprg 8170 . . . . . . . . . . . . 13 |- ( ( v e. P. /\ w e. P. /\ C e. R. ) -> ( ( C +R [ <. v , 1P >. ] ~R ) <R ( C +R [ <. w , 1P >. ] ~R ) <-> v <P w ) )
3531, 32, 33, 34syl3anc 1278 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> ( ( C +R [ <. v , 1P >. ] ~R ) <R ( C +R [ <. w , 1P >. ] ~R ) <-> v <P w ) )
3630, 35mpbid 147 . . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> v <P w )
37 equcom 1758 . . . . . . . . . . . . 13 |- ( w = a <-> a = w )
38 bicom 140 . . . . . . . . . . . . 13 |- ( ( -. v <P w <-> -. v <P a ) <-> ( -. v <P a <-> -. v <P w ) )
3917, 37, 383imtr3i 200 . . . . . . . . . . . 12 |- ( a = w -> ( -. v <P a <-> -. v <P w ) )
40 simp-4r 548 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> A. a e. B -. v <P a )
41 simpllr 540 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> y e. A )
4229, 41eqeltrd 2315 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> ( C +R [ <. w , 1P >. ] ~R ) e. A )
431rabeq2i 2818 . . . . . . . . . . . . 13 |- ( w e. B <-> ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) e. A ) )
4432, 42, 43sylanbrc 421 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> w e. B )
4539, 40, 44rspcdva 2934 . . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> -. v <P w )
4636, 45pm2.21fal 1422 . . . . . . . . . 10 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) /\ ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) ) -> F. )
4727, 46rexlimddv 2673 . . . . . . . . 9 |- ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> F. )
4847inegd 1421 . . . . . . . 8 |- ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) -> -. ( C +R [ <. v , 1P >. ] ~R ) <R y )
4948ralrimiva 2623 . . . . . . 7 |- ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) -> A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) <R y )
5049ex 115 . . . . . 6 |- ( ( ph /\ v e. P. ) -> ( A. a e. B -. v <P a -> A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) <R y ) )
5118, 50biimtrid 152 . . . . 5 |- ( ( ph /\ v e. P. ) -> ( A. w e. B -. v <P w -> A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) <R y ) )
52 nfv 1581 . . . . . . . . . . . . . 14 |- F/ w ( ph /\ v e. P. )
53 nfra1 2581 . . . . . . . . . . . . . 14 |- F/ w A. w e. P. ( w <P v -> E. u e. B w <P u )
5452, 53nfan 1618 . . . . . . . . . . . . 13 |- F/ w ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) )
55 nfv 1581 . . . . . . . . . . . . 13 |- F/ w y e. R.
5654, 55nfan 1618 . . . . . . . . . . . 12 |- F/ w ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. )
57 nfv 1581 . . . . . . . . . . . 12 |- F/ w y <R ( C +R [ <. v , 1P >. ] ~R )
5856, 57nfan 1618 . . . . . . . . . . 11 |- F/ w ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) )
59 nfv 1581 . . . . . . . . . . 11 |- F/ w ( C +R -1R ) <R y
6058, 59nfan 1618 . . . . . . . . . 10 |- F/ w ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y )
61 simp-6r 552 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) -> A. w e. P. ( w <P v -> E. u e. B w <P u ) )
62 simplr 533 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) -> w e. P. )
63 simpr 110 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) -> ( C +R [ <. w , 1P >. ] ~R ) = y )
64 simp-4r 548 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) -> y <R ( C +R [ <. v , 1P >. ] ~R ) )
6563, 64eqbrtrd 4152 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) -> ( C +R [ <. w , 1P >. ] ~R ) <R ( C +R [ <. v , 1P >. ] ~R ) )
66 simp-7r 554 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) -> v e. P. )
679ad4antr 498 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) -> C e. R. )
6867ad2antrr 492 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) -> C e. R. )
69 ltpsrprg 8170 . . . . . . . . . . . . . . 15 |- ( ( w e. P. /\ v e. P. /\ C e. R. ) -> ( ( C +R [ <. w , 1P >. ] ~R ) <R ( C +R [ <. v , 1P >. ] ~R ) <-> w <P v ) )
7062, 66, 68, 69syl3anc 1278 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) -> ( ( C +R [ <. w , 1P >. ] ~R ) <R ( C +R [ <. v , 1P >. ] ~R ) <-> w <P v ) )
7165, 70mpbid 147 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) -> w <P v )
72 rsp 2597 . . . . . . . . . . . . 13 |- ( A. w e. P. ( w <P v -> E. u e. B w <P u ) -> ( w e. P. -> ( w <P v -> E. u e. B w <P u ) ) )
7361, 62, 71, 72syl3c 63 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) -> E. u e. B w <P u )
74 breq2 4134 . . . . . . . . . . . . 13 |- ( u = b -> ( w <P u <-> w <P b ) )
7574cbvrexv 2787 . . . . . . . . . . . 12 |- ( E. u e. B w <P u <-> E. b e. B w <P b )
7673, 75sylib 122 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) -> E. b e. B w <P b )
77 simprl 535 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) /\ ( b e. B /\ w <P b ) ) -> b e. B )
78 opeq1 3904 . . . . . . . . . . . . . . . . . 18 |- ( w = b -> <. w , 1P >. = <. b , 1P >. )
7978eceq1d 6843 . . . . . . . . . . . . . . . . 17 |- ( w = b -> [ <. w , 1P >. ] ~R = [ <. b , 1P >. ] ~R )
8079oveq2d 6101 . . . . . . . . . . . . . . . 16 |- ( w = b -> ( C +R [ <. w , 1P >. ] ~R ) = ( C +R [ <. b , 1P >. ] ~R ) )
8180eleq1d 2307 . . . . . . . . . . . . . . 15 |- ( w = b -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A <-> ( C +R [ <. b , 1P >. ] ~R ) e. A ) )
8281, 1elrab2 2985 . . . . . . . . . . . . . 14 |- ( b e. B <-> ( b e. P. /\ ( C +R [ <. b , 1P >. ] ~R ) e. A ) )
8377, 82sylib 122 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) /\ ( b e. B /\ w <P b ) ) -> ( b e. P. /\ ( C +R [ <. b , 1P >. ] ~R ) e. A ) )
8483simprd 114 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) /\ ( b e. B /\ w <P b ) ) -> ( C +R [ <. b , 1P >. ] ~R ) e. A )
85 simplr 533 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) /\ ( b e. B /\ w <P b ) ) -> ( C +R [ <. w , 1P >. ] ~R ) = y )
86 simprr 537 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) /\ ( b e. B /\ w <P b ) ) -> w <P b )
87 simpllr 540 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) /\ ( b e. B /\ w <P b ) ) -> w e. P. )
8883simpld 112 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) /\ ( b e. B /\ w <P b ) ) -> b e. P. )
8967ad3antrrr 496 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) /\ ( b e. B /\ w <P b ) ) -> C e. R. )
90 ltpsrprg 8170 . . . . . . . . . . . . . . 15 |- ( ( w e. P. /\ b e. P. /\ C e. R. ) -> ( ( C +R [ <. w , 1P >. ] ~R ) <R ( C +R [ <. b , 1P >. ] ~R ) <-> w <P b ) )
9187, 88, 89, 90syl3anc 1278 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) /\ ( b e. B /\ w <P b ) ) -> ( ( C +R [ <. w , 1P >. ] ~R ) <R ( C +R [ <. b , 1P >. ] ~R ) <-> w <P b ) )
9286, 91mpbird 167 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) /\ ( b e. B /\ w <P b ) ) -> ( C +R [ <. w , 1P >. ] ~R ) <R ( C +R [ <. b , 1P >. ] ~R ) )
9385, 92eqbrtrrd 4154 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) /\ ( b e. B /\ w <P b ) ) -> y <R ( C +R [ <. b , 1P >. ] ~R ) )
94 breq2 4134 . . . . . . . . . . . . 13 |- ( z = ( C +R [ <. b , 1P >. ] ~R ) -> ( y <R z <-> y <R ( C +R [ <. b , 1P >. ] ~R ) ) )
9594rspcev 2929 . . . . . . . . . . . 12 |- ( ( ( C +R [ <. b , 1P >. ] ~R ) e. A /\ y <R ( C +R [ <. b , 1P >. ] ~R ) ) -> E. z e. A y <R z )
9684, 93, 95syl2anc 415 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) /\ ( b e. B /\ w <P b ) ) -> E. z e. A y <R z )
9776, 96rexlimddv 2673 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) /\ w e. P. ) /\ ( C +R [ <. w , 1P >. ] ~R ) = y ) -> E. z e. A y <R z )
98 simpr 110 . . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) -> ( C +R -1R ) <R y )
9967, 23syl 14 . . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) -> ( ( C +R -1R ) <R y <-> E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y ) )
10098, 99mpbid 147 . . . . . . . . . 10 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) -> E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y )
10160, 97, 100r19.29af 2692 . . . . . . . . 9 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ ( C +R -1R ) <R y ) -> E. z e. A y <R z )
1023ad5antr 500 . . . . . . . . . 10 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ y <R C ) -> C e. A )
103 breq2 4134 . . . . . . . . . . 11 |- ( z = C -> ( y <R z <-> y <R C ) )
104103rspcev 2929 . . . . . . . . . 10 |- ( ( C e. A /\ y <R C ) -> E. z e. A y <R z )
105102, 104sylancom 424 . . . . . . . . 9 |- ( ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) /\ y <R C ) -> E. z e. A y <R z )
106 ltm1sr 8144 . . . . . . . . . . . 12 |- ( C e. R. -> ( C +R -1R ) <R C )
1078, 106syl 14 . . . . . . . . . . 11 |- ( ph -> ( C +R -1R ) <R C )
108107ad4antr 498 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) -> ( C +R -1R ) <R C )
1099ad3antrrr 496 . . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) -> C e. R. )
110 m1r 8119 . . . . . . . . . . . 12 |- -1R e. R.
111 addclsr 8120 . . . . . . . . . . . 12 |- ( ( C e. R. /\ -1R e. R. ) -> ( C +R -1R ) e. R. )
112109, 110, 111sylancl 417 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) -> ( C +R -1R ) e. R. )
113 simplr 533 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) -> y e. R. )
114 sowlin 4465 . . . . . . . . . . . 12 |- ( ( <R Or R. /\ ( ( C +R -1R ) e. R. /\ C e. R. /\ y e. R. ) ) -> ( ( C +R -1R ) <R C -> ( ( C +R -1R ) <R y \/ y <R C ) ) )
11519, 114mpan 428 . . . . . . . . . . 11 |- ( ( ( C +R -1R ) e. R. /\ C e. R. /\ y e. R. ) -> ( ( C +R -1R ) <R C -> ( ( C +R -1R ) <R y \/ y <R C ) ) )
116112, 109, 113, 115syl3anc 1278 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) -> ( ( C +R -1R ) <R C -> ( ( C +R -1R ) <R y \/ y <R C ) ) )
117108, 116mpd 13 . . . . . . . . 9 |- ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) -> ( ( C +R -1R ) <R y \/ y <R C ) )
118101, 105, 117mpjaodan 810 . . . . . . . 8 |- ( ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) /\ y <R ( C +R [ <. v , 1P >. ] ~R ) ) -> E. z e. A y <R z )
119118ex 115 . . . . . . 7 |- ( ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) /\ y e. R. ) -> ( y <R ( C +R [ <. v , 1P >. ] ~R ) -> E. z e. A y <R z ) )
120119ralrimiva 2623 . . . . . 6 |- ( ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) -> A. y e. R. ( y <R ( C +R [ <. v , 1P >. ] ~R ) -> E. z e. A y <R z ) )
121120ex 115 . . . . 5 |- ( ( ph /\ v e. P. ) -> ( A. w e. P. ( w <P v -> E. u e. B w <P u ) -> A. y e. R. ( y <R ( C +R [ <. v , 1P >. ] ~R ) -> E. z e. A y <R z ) ) )
12251, 121anim12d 335 . . . 4 |- ( ( ph /\ v e. P. ) -> ( ( A. w e. B -. v <P w /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) -> ( A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) <R y /\ A. y e. R. ( y <R ( C +R [ <. v , 1P >. ] ~R ) -> E. z e. A y <R z ) ) ) )
123 breq1 4133 . . . . . . . 8 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( x <R y <-> ( C +R [ <. v , 1P >. ] ~R ) <R y ) )
124123notbid 677 . . . . . . 7 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( -. x <R y <-> -. ( C +R [ <. v , 1P >. ] ~R ) <R y ) )
125124ralbidv 2550 . . . . . 6 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( A. y e. A -. x <R y <-> A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) <R y ) )
126 breq2 4134 . . . . . . . 8 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( y <R x <-> y <R ( C +R [ <. v , 1P >. ] ~R ) ) )
127126imbi1d 231 . . . . . . 7 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( ( y <R x -> E. z e. A y <R z ) <-> ( y <R ( C +R [ <. v , 1P >. ] ~R ) -> E. z e. A y <R z ) ) )
128127ralbidv 2550 . . . . . 6 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( A. y e. R. ( y <R x -> E. z e. A y <R z ) <-> A. y e. R. ( y <R ( C +R [ <. v , 1P >. ] ~R ) -> E. z e. A y <R z ) ) )
129125, 128anbi12d 477 . . . . 5 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( ( A. y e. A -. x <R y /\ A. y e. R. ( y <R x -> E. z e. A y <R z ) ) <-> ( A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) <R y /\ A. y e. R. ( y <R ( C +R [ <. v , 1P >. ] ~R ) -> E. z e. A y <R z ) ) ) )
130129rspcev 2929 . . . 4 |- ( ( ( C +R [ <. v , 1P >. ] ~R ) e. R. /\ ( A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) <R y /\ A. y e. R. ( y <R ( C +R [ <. v , 1P >. ] ~R ) -> E. z e. A y <R z ) ) ) -> E. x e. R. ( A. y e. A -. x <R y /\ A. y e. R. ( y <R x -> E. z e. A y <R z ) ) )
13115, 122, 130syl6an 1483 . . 3 |- ( ( ph /\ v e. P. ) -> ( ( A. w e. B -. v <P w /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) -> E. x e. R. ( A. y e. A -. x <R y /\ A. y e. R. ( y <R x -> E. z e. A y <R z ) ) ) )
132131rexlimdva 2668 . 2 |- ( ph -> ( E. v e. P. ( A. w e. B -. v <P w /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) -> E. x e. R. ( A. y e. A -. x <R y /\ A. y e. R. ( y <R x -> E. z e. A y <R z ) ) ) )
1336, 132mpd 13 1 |- ( ph -> E. x e. R. ( A. y e. A -. x <R y /\ A. y e. R. ( y <R x -> E. z e. A y <R z ) ) )
Colors of variables:    wff set class
This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 720   /\ w3a 1009   = wceq 1402   F. wfal 1407   e. wcel 2209   A.wral 2528   E.wrex 2529   {crab 2532   C_ wss 3220   <.cop 3712   class class class wbr 4130   Or wor 4440  (class class class)co 6085   [cec 6805   P.cnp 7658   1Pc1p 7659   <P cltp 7662   ~R cer 7663   R.cnr 7664   -1Rcm1r 7667   +R cplr 7668   <R cltr 7670
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735
This proof depends on definitions:  df-bi 117  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-eprel 4434  df-id 4438  df-po 4441  df-iso 4442  df-iord 4511  df-on 4513  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-ov 6088  df-oprab 6089  df-mpo 6090  df-1st 6374  df-2nd 6375  df-recs 6576  df-irdg 6641  df-1o 6687  df-2o 6688  df-oadd 6691  df-omul 6692  df-er 6807  df-ec 6809  df-qs 6813  df-ni 7671  df-pli 7672  df-mi 7673  df-lti 7674  df-plpq 7711  df-mpq 7712  df-enq 7714  df-nqqs 7715  df-plqqs 7716  df-mqqs 7717  df-1nqqs 7718  df-rq 7719  df-ltnqqs 7720  df-enq0 7791  df-nq0 7792  df-0nq0 7793  df-plq0 7794  df-mq0 7795  df-inp 7833  df-i1p 7834  df-iplp 7835  df-imp 7836  df-iltp 7837  df-enr 8093  df-nr 8094  df-plr 8095  df-mr 8096  df-ltr 8097  df-0r 8098  df-1r 8099  df-m1r 8100
This theorem is used by:  suplocsr  8176
  Copyright terms: Public domain W3C validator