ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  suplocsrlem Unicode version
Theorem suplocsrlem 7770
Description: Lemma for suplocsr 7771. 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 7769 . 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 109 . . . . . . 7 |- ( ( ph /\ v e. P. ) -> v e. P. )
82, 3sseldd 3148 . . . . . . . 8 |- ( ph -> C e. R. )
98adantr 274 . . . . . . 7 |- ( ( ph /\ v e. P. ) -> C e. R. )
10 mappsrprg 7766 . . . . . . 7 |- ( ( v e. P. /\ C e. R. ) -> ( C +R -1R ) <R ( C +R [ <. v , 1P >. ] ~R ) )
117, 9, 10syl2anc 409 . . . . . 6 |- ( ( ph /\ v e. P. ) -> ( C +R -1R ) <R ( C +R [ <. v , 1P >. ] ~R ) )
12 ltrelsr 7700 . . . . . . 7 |- <R C_ ( R. X. R. )
1312brel 4663 . . . . . 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 113 . . . 4 |- ( ( ph /\ v e. P. ) -> ( C +R [ <. v , 1P >. ] ~R ) e. R. )
16 breq2 3993 . . . . . . . 8 |- ( w = a -> ( v <P w <-> v <P a ) )
1716notbid 662 . . . . . . 7 |- ( w = a -> ( -. v <P w <-> -. v <P a ) )
1817cbvralv 2696 . . . . . 6 |- ( A. w e. B -. v <P w <-> A. a e. B -. v <P a )
19 ltsosr 7726 . . . . . . . . . . . . . . 15 |- <R Or R.
2019, 12sotri 5006 . . . . . . . . . . . . . 14 |- ( ( ( C +R -1R ) <R ( C +R [ <. v , 1P >. ] ~R ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> ( C +R -1R ) <R y )
2111, 20sylan 281 . . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. P. ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> ( C +R -1R ) <R y )
229adantr 274 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. P. ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> C e. R. )
23 map2psrprg 7767 . . . . . . . . . . . . . 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 146 . . . . . . . . . . . 12 |- ( ( ( ph /\ v e. P. ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y )
2625adantlr 474 . . . . . . . . . . 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 474 . . . . . . . . . 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 525 . . . . . . . . . . . . 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 527 . . . . . . . . . . . . 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 4017 . . . . . . . . . . . 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 491 . . . . . . . . . . . . 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 526 . . . . . . . . . . . . 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 491 . . . . . . . . . . . . 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 7765 . . . . . . . . . . . . 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 1233 . . . . . . . . . . . 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 146 . . . . . . . . . . 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 1699 . . . . . . . . . . . . 13 |- ( w = a <-> a = w )
38 bicom 139 . . . . . . . . . . . . 13 |- ( ( -. v <P w <-> -. v <P a ) <-> ( -. v <P a <-> -. v <P w ) )
3917, 37, 383imtr3i 199 . . . . . . . . . . . 12 |- ( a = w -> ( -. v <P a <-> -. v <P w ) )
40 simp-4r 537 . . . . . . . . . . . 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 529 . . . . . . . . . . . . . 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 2247 . . . . . . . . . . . . 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 2727 . . . . . . . . . . . . 13 |- ( w e. B <-> ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) e. A ) )
4432, 42, 43sylanbrc 415 . . . . . . . . . . . 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 2839 . . . . . . . . . . 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 1368 . . . . . . . . . 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 2592 . . . . . . . . 9 |- ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> F. )
4847inegd 1367 . . . . . . . 8 |- ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) -> -. ( C +R [ <. v , 1P >. ] ~R ) <R y )
4948ralrimiva 2543 . . . . . . 7 |- ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) -> A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) <R y )
5049ex 114 . . . . . 6 |- ( ( ph /\ v e. P. ) -> ( A. a e. B -. v <P a -> A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) <R y ) )
5118, 50syl5bi 151 . . . . 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 1521 . . . . . . . . . . . . . 14 |- F/ w ( ph /\ v e. P. )
53 nfra1 2501 . . . . . . . . . . . . . 14 |- F/ w A. w e. P. ( w <P v -> E. u e. B w <P u )
5452, 53nfan 1558 . . . . . . . . . . . . 13 |- F/ w ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) )
55 nfv 1521 . . . . . . . . . . . . 13 |- F/ w y e. R.
5654, 55nfan 1558 . . . . . . . . . . . 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 1521 . . . . . . . . . . . 12 |- F/ w y <R ( C +R [ <. v , 1P >. ] ~R )
5856, 57nfan 1558 . . . . . . . . . . 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 1521 . . . . . . . . . . 11 |- F/ w ( C +R -1R ) <R y
6058, 59nfan 1558 . . . . . . . . . 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 541 . . . . . . . . . . . . 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 525 . . . . . . . . . . . . 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 109 . . . . . . . . . . . . . . 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 537 . . . . . . . . . . . . . . 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 4011 . . . . . . . . . . . . . 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 543 . . . . . . . . . . . . . . 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 491 . . . . . . . . . . . . . . . 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 485 . . . . . . . . . . . . . . 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 7765 . . . . . . . . . . . . . . 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 1233 . . . . . . . . . . . . . 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 146 . . . . . . . . . . . . 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 2517 . . . . . . . . . . . . 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 3993 . . . . . . . . . . . . 13 |- ( u = b -> ( w <P u <-> w <P b ) )
7574cbvrexv 2697 . . . . . . . . . . . 12 |- ( E. u e. B w <P u <-> E. b e. B w <P b )
7673, 75sylib 121 . . . . . . . . . . 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 526 . . . . . . . . . . . . . 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 3765 . . . . . . . . . . . . . . . . . 18 |- ( w = b -> <. w , 1P >. = <. b , 1P >. )
7978eceq1d 6549 . . . . . . . . . . . . . . . . 17 |- ( w = b -> [ <. w , 1P >. ] ~R = [ <. b , 1P >. ] ~R )
8079oveq2d 5869 . . . . . . . . . . . . . . . 16 |- ( w = b -> ( C +R [ <. w , 1P >. ] ~R ) = ( C +R [ <. b , 1P >. ] ~R ) )
8180eleq1d 2239 . . . . . . . . . . . . . . 15 |- ( w = b -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A <-> ( C +R [ <. b , 1P >. ] ~R ) e. A ) )
8281, 1elrab2 2889 . . . . . . . . . . . . . 14 |- ( b e. B <-> ( b e. P. /\ ( C +R [ <. b , 1P >. ] ~R ) e. A ) )
8377, 82sylib 121 . . . . . . . . . . . . 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 113 . . . . . . . . . . . 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 525 . . . . . . . . . . . . 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 527 . . . . . . . . . . . . . 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 529 . . . . . . . . . . . . . . 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 111 . . . . . . . . . . . . . . 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 489 . . . . . . . . . . . . . . 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 7765 . . . . . . . . . . . . . . 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 1233 . . . . . . . . . . . . . 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 166 . . . . . . . . . . . . 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 4013 . . . . . . . . . . . 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 3993 . . . . . . . . . . . . 13 |- ( z = ( C +R [ <. b , 1P >. ] ~R ) -> ( y <R z <-> y <R ( C +R [ <. b , 1P >. ] ~R ) ) )
9594rspcev 2834 . . . . . . . . . . . 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 409 . . . . . . . . . . 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 2592 . . . . . . . . . 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 109 . . . . . . . . . . 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 146 . . . . . . . . . 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 2611 . . . . . . . . 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 493 . . . . . . . . . 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 3993 . . . . . . . . . . 11 |- ( z = C -> ( y <R z <-> y <R C ) )
104103rspcev 2834 . . . . . . . . . 10 |- ( ( C e. A /\ y <R C ) -> E. z e. A y <R z )
105102, 104sylancom 418 . . . . . . . . 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 7739 . . . . . . . . . . . 12 |- ( C e. R. -> ( C +R -1R ) <R C )
1078, 106syl 14 . . . . . . . . . . 11 |- ( ph -> ( C +R -1R ) <R C )
108107ad4antr 491 . . . . . . . . . 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 489 . . . . . . . . . . . 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 7714 . . . . . . . . . . . 12 |- -1R e. R.
111 addclsr 7715 . . . . . . . . . . . 12 |- ( ( C e. R. /\ -1R e. R. ) -> ( C +R -1R ) e. R. )
112109, 110, 111sylancl 411 . . . . . . . . . . 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 525 . . . . . . . . . . 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 4305 . . . . . . . . . . . 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 422 . . . . . . . . . . 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 1233 . . . . . . . . . 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 793 . . . . . . . 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 114 . . . . . . 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 2543 . . . . . 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 114 . . . . 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 333 . . . 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 3992 . . . . . . . 8 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( x <R y <-> ( C +R [ <. v , 1P >. ] ~R ) <R y ) )
124123notbid 662 . . . . . . 7 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( -. x <R y <-> -. ( C +R [ <. v , 1P >. ] ~R ) <R y ) )
125124ralbidv 2470 . . . . . 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 3993 . . . . . . . 8 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( y <R x <-> y <R ( C +R [ <. v , 1P >. ] ~R ) ) )
127126imbi1d 230 . . . . . . 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 2470 . . . . . 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 470 . . . . 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 2834 . . . 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 1427 . . 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 2587 . 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
Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 703   /\ w3a 973   = wceq 1348   F. wfal 1353   e. wcel 2141   A.wral 2448   E.wrex 2449   {crab 2452   C_ wss 3121   <.cop 3586   class class class wbr 3989   Or wor 4280  (class class class)co 5853   [cec 6511   P.cnp 7253   1Pc1p 7254   <P cltp 7257   ~R cer 7258   R.cnr 7259   -1Rcm1r 7262   +R cplr 7263   <R cltr 7265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-eprel 4274  df-id 4278  df-po 4281  df-iso 4282  df-iord 4351  df-on 4353  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-recs 6284  df-irdg 6349  df-1o 6395  df-2o 6396  df-oadd 6399  df-omul 6400  df-er 6513  df-ec 6515  df-qs 6519  df-ni 7266  df-pli 7267  df-mi 7268  df-lti 7269  df-plpq 7306  df-mpq 7307  df-enq 7309  df-nqqs 7310  df-plqqs 7311  df-mqqs 7312  df-1nqqs 7313  df-rq 7314  df-ltnqqs 7315  df-enq0 7386  df-nq0 7387  df-0nq0 7388  df-plq0 7389  df-mq0 7390  df-inp 7428  df-i1p 7429  df-iplp 7430  df-imp 7431  df-iltp 7432  df-enr 7688  df-nr 7689  df-plr 7690  df-mr 7691  df-ltr 7692  df-0r 7693  df-1r 7694  df-m1r 7695
This theorem is referenced by:  suplocsr  7771
  Copyright terms: Public domain W3C validator