ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  suplocsrlem Unicode version
Theorem suplocsrlem 7616
Description: Lemma for suplocsr 7617. 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 7615 . 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 3098 . . . . . . . 8 |- ( ph -> C e. R. )
98adantr 274 . . . . . . 7 |- ( ( ph /\ v e. P. ) -> C e. R. )
10 mappsrprg 7612 . . . . . . 7 |- ( ( v e. P. /\ C e. R. ) -> ( C +R -1R ) <R ( C +R [ <. v , 1P >. ] ~R ) )
117, 9, 10syl2anc 408 . . . . . 6 |- ( ( ph /\ v e. P. ) -> ( C +R -1R ) <R ( C +R [ <. v , 1P >. ] ~R ) )
12 ltrelsr 7546 . . . . . . 7 |- <R C_ ( R. X. R. )
1312brel 4591 . . . . . 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 3933 . . . . . . . 8 |- ( w = a -> ( v <P w <-> v <P a ) )
1716notbid 656 . . . . . . 7 |- ( w = a -> ( -. v <P w <-> -. v <P a ) )
1817cbvralv 2654 . . . . . 6 |- ( A. w e. B -. v <P w <-> A. a e. B -. v <P a )
19 ltsosr 7572 . . . . . . . . . . . . . . 15 |- <R Or R.
2019, 12sotri 4934 . . . . . . . . . . . . . 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 7613 . . . . . . . . . . . . . 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 468 . . . . . . . . . . 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 468 . . . . . . . . . 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 519 . . . . . . . . . . . . 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 521 . . . . . . . . . . . . 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 3956 . . . . . . . . . . . 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 485 . . . . . . . . . . . . 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 520 . . . . . . . . . . . . 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 485 . . . . . . . . . . . . 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 7611 . . . . . . . . . . . . 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 1216 . . . . . . . . . . . 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 1682 . . . . . . . . . . . . 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 531 . . . . . . . . . . . 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 523 . . . . . . . . . . . . . 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 2216 . . . . . . . . . . . . 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 2683 . . . . . . . . . . . . 13 |- ( w e. B <-> ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) e. A ) )
4432, 42, 43sylanbrc 413 . . . . . . . . . . . 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 2794 . . . . . . . . . . 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 1351 . . . . . . . . . 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 2554 . . . . . . . . 9 |- ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> F. )
4847inegd 1350 . . . . . . . 8 |- ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) -> -. ( C +R [ <. v , 1P >. ] ~R ) <R y )
4948ralrimiva 2505 . . . . . . 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 1508 . . . . . . . . . . . . . 14 |- F/ w ( ph /\ v e. P. )
53 nfra1 2466 . . . . . . . . . . . . . 14 |- F/ w A. w e. P. ( w <P v -> E. u e. B w <P u )
5452, 53nfan 1544 . . . . . . . . . . . . 13 |- F/ w ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) )
55 nfv 1508 . . . . . . . . . . . . 13 |- F/ w y e. R.
5654, 55nfan 1544 . . . . . . . . . . . 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 1508 . . . . . . . . . . . 12 |- F/ w y <R ( C +R [ <. v , 1P >. ] ~R )
5856, 57nfan 1544 . . . . . . . . . . 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 1508 . . . . . . . . . . 11 |- F/ w ( C +R -1R ) <R y
6058, 59nfan 1544 . . . . . . . . . 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 535 . . . . . . . . . . . . 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 519 . . . . . . . . . . . . 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 531 . . . . . . . . . . . . . . 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 3950 . . . . . . . . . . . . . 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 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 ) -> v e. P. )
679ad4antr 485 . . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . 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 7611 . . . . . . . . . . . . . . 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 1216 . . . . . . . . . . . . . 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 2480 . . . . . . . . . . . . 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 3933 . . . . . . . . . . . . 13 |- ( u = b -> ( w <P u <-> w <P b ) )
7574cbvrexv 2655 . . . . . . . . . . . 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 520 . . . . . . . . . . . . . 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 3705 . . . . . . . . . . . . . . . . . 18 |- ( w = b -> <. w , 1P >. = <. b , 1P >. )
7978eceq1d 6465 . . . . . . . . . . . . . . . . 17 |- ( w = b -> [ <. w , 1P >. ] ~R = [ <. b , 1P >. ] ~R )
8079oveq2d 5790 . . . . . . . . . . . . . . . 16 |- ( w = b -> ( C +R [ <. w , 1P >. ] ~R ) = ( C +R [ <. b , 1P >. ] ~R ) )
8180eleq1d 2208 . . . . . . . . . . . . . . 15 |- ( w = b -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A <-> ( C +R [ <. b , 1P >. ] ~R ) e. A ) )
8281, 1elrab2 2843 . . . . . . . . . . . . . 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 519 . . . . . . . . . . . . 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 521 . . . . . . . . . . . . . 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 523 . . . . . . . . . . . . . . 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 483 . . . . . . . . . . . . . . 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 7611 . . . . . . . . . . . . . . 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 1216 . . . . . . . . . . . . . 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 3952 . . . . . . . . . . . 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 3933 . . . . . . . . . . . . 13 |- ( z = ( C +R [ <. b , 1P >. ] ~R ) -> ( y <R z <-> y <R ( C +R [ <. b , 1P >. ] ~R ) ) )
9594rspcev 2789 . . . . . . . . . . . 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 408 . . . . . . . . . . 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 2554 . . . . . . . . . 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 2573 . . . . . . . . 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 487 . . . . . . . . . 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 3933 . . . . . . . . . . 11 |- ( z = C -> ( y <R z <-> y <R C ) )
104103rspcev 2789 . . . . . . . . . 10 |- ( ( C e. A /\ y <R C ) -> E. z e. A y <R z )
105102, 104sylancom 416 . . . . . . . . 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 7585 . . . . . . . . . . . 12 |- ( C e. R. -> ( C +R -1R ) <R C )
1078, 106syl 14 . . . . . . . . . . 11 |- ( ph -> ( C +R -1R ) <R C )
108107ad4antr 485 . . . . . . . . . 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 483 . . . . . . . . . . . 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 7560 . . . . . . . . . . . 12 |- -1R e. R.
111 addclsr 7561 . . . . . . . . . . . 12 |- ( ( C e. R. /\ -1R e. R. ) -> ( C +R -1R ) e. R. )
112109, 110, 111sylancl 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 ) e. R. )
113 simplr 519 . . . . . . . . . . 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 4242 . . . . . . . . . . . 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 420 . . . . . . . . . . 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 1216 . . . . . . . . . 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 787 . . . . . . . 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 2505 . . . . . 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 3932 . . . . . . . 8 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( x <R y <-> ( C +R [ <. v , 1P >. ] ~R ) <R y ) )
124123notbid 656 . . . . . . 7 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( -. x <R y <-> -. ( C +R [ <. v , 1P >. ] ~R ) <R y ) )
125124ralbidv 2437 . . . . . 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 3933 . . . . . . . 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 2437 . . . . . 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 464 . . . . 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 2789 . . . 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 1410 . . 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 2549 . 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 697   /\ w3a 962   = wceq 1331   F. wfal 1336   e. wcel 1480   A.wral 2416   E.wrex 2417   {crab 2420   C_ wss 3071   <.cop 3530   class class class wbr 3929   Or wor 4217  (class class class)co 5774   [cec 6427   P.cnp 7099   1Pc1p 7100   <P cltp 7103   ~R cer 7104   R.cnr 7105   -1Rcm1r 7108   +R cplr 7109   <R cltr 7111
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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-eprel 4211  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-irdg 6267  df-1o 6313  df-2o 6314  df-oadd 6317  df-omul 6318  df-er 6429  df-ec 6431  df-qs 6435  df-ni 7112  df-pli 7113  df-mi 7114  df-lti 7115  df-plpq 7152  df-mpq 7153  df-enq 7155  df-nqqs 7156  df-plqqs 7157  df-mqqs 7158  df-1nqqs 7159  df-rq 7160  df-ltnqqs 7161  df-enq0 7232  df-nq0 7233  df-0nq0 7234  df-plq0 7235  df-mq0 7236  df-inp 7274  df-i1p 7275  df-iplp 7276  df-imp 7277  df-iltp 7278  df-enr 7534  df-nr 7535  df-plr 7536  df-mr 7537  df-ltr 7538  df-0r 7539  df-1r 7540  df-m1r 7541
This theorem is referenced by:  suplocsr  7617
  Copyright terms: Public domain W3C validator