ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  suplocsrlem Unicode version
Theorem suplocsrlem 7640
Description: Lemma for suplocsr 7641. 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 7639 . 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 3103 . . . . . . . 8 |- ( ph -> C e. R. )
98adantr 274 . . . . . . 7 |- ( ( ph /\ v e. P. ) -> C e. R. )
10 mappsrprg 7636 . . . . . . 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 7570 . . . . . . 7 |- <R C_ ( R. X. R. )
1312brel 4599 . . . . . 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 3941 . . . . . . . 8 |- ( w = a -> ( v <P w <-> v <P a ) )
1716notbid 657 . . . . . . 7 |- ( w = a -> ( -. v <P w <-> -. v <P a ) )
1817cbvralv 2657 . . . . . 6 |- ( A. w e. B -. v <P w <-> A. a e. B -. v <P a )
19 ltsosr 7596 . . . . . . . . . . . . . . 15 |- <R Or R.
2019, 12sotri 4942 . . . . . . . . . . . . . 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 7637 . . . . . . . . . . . . . 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 469 . . . . . . . . . . 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 469 . . . . . . . . . 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 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 ) ) -> ( C +R [ <. v , 1P >. ] ~R ) <R y )
29 simprr 522 . . . . . . . . . . . . 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 3964 . . . . . . . . . . . 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 486 . . . . . . . . . . . . 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 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 ) ) -> w e. P. )
339ad4antr 486 . . . . . . . . . . . . 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 7635 . . . . . . . . . . . . 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 1217 . . . . . . . . . . . 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 1683 . . . . . . . . . . . . 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 532 . . . . . . . . . . . 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 524 . . . . . . . . . . . . . 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 2217 . . . . . . . . . . . . 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 2686 . . . . . . . . . . . . 13 |- ( w e. B <-> ( w e. P. /\ ( C +R [ <. w , 1P >. ] ~R ) e. A ) )
4432, 42, 43sylanbrc 414 . . . . . . . . . . . 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 2798 . . . . . . . . . . 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 1352 . . . . . . . . . 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 2557 . . . . . . . . 9 |- ( ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) /\ ( C +R [ <. v , 1P >. ] ~R ) <R y ) -> F. )
4847inegd 1351 . . . . . . . 8 |- ( ( ( ( ph /\ v e. P. ) /\ A. a e. B -. v <P a ) /\ y e. A ) -> -. ( C +R [ <. v , 1P >. ] ~R ) <R y )
4948ralrimiva 2508 . . . . . . 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 1509 . . . . . . . . . . . . . 14 |- F/ w ( ph /\ v e. P. )
53 nfra1 2469 . . . . . . . . . . . . . 14 |- F/ w A. w e. P. ( w <P v -> E. u e. B w <P u )
5452, 53nfan 1545 . . . . . . . . . . . . 13 |- F/ w ( ( ph /\ v e. P. ) /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) )
55 nfv 1509 . . . . . . . . . . . . 13 |- F/ w y e. R.
5654, 55nfan 1545 . . . . . . . . . . . 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 1509 . . . . . . . . . . . 12 |- F/ w y <R ( C +R [ <. v , 1P >. ] ~R )
5856, 57nfan 1545 . . . . . . . . . . 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 1509 . . . . . . . . . . 11 |- F/ w ( C +R -1R ) <R y
6058, 59nfan 1545 . . . . . . . . . 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 536 . . . . . . . . . . . . 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 520 . . . . . . . . . . . . 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 532 . . . . . . . . . . . . . . 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 3958 . . . . . . . . . . . . . 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 538 . . . . . . . . . . . . . . 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 486 . . . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . . 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 7635 . . . . . . . . . . . . . . 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 1217 . . . . . . . . . . . . . 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 2483 . . . . . . . . . . . . 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 3941 . . . . . . . . . . . . 13 |- ( u = b -> ( w <P u <-> w <P b ) )
7574cbvrexv 2658 . . . . . . . . . . . 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 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 ) ) -> b e. B )
78 opeq1 3713 . . . . . . . . . . . . . . . . . 18 |- ( w = b -> <. w , 1P >. = <. b , 1P >. )
7978eceq1d 6473 . . . . . . . . . . . . . . . . 17 |- ( w = b -> [ <. w , 1P >. ] ~R = [ <. b , 1P >. ] ~R )
8079oveq2d 5798 . . . . . . . . . . . . . . . 16 |- ( w = b -> ( C +R [ <. w , 1P >. ] ~R ) = ( C +R [ <. b , 1P >. ] ~R ) )
8180eleq1d 2209 . . . . . . . . . . . . . . 15 |- ( w = b -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A <-> ( C +R [ <. b , 1P >. ] ~R ) e. A ) )
8281, 1elrab2 2847 . . . . . . . . . . . . . 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 520 . . . . . . . . . . . . 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 522 . . . . . . . . . . . . . 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 524 . . . . . . . . . . . . . . 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 484 . . . . . . . . . . . . . . 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 7635 . . . . . . . . . . . . . . 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 1217 . . . . . . . . . . . . . 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 3960 . . . . . . . . . . . 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 3941 . . . . . . . . . . . . 13 |- ( z = ( C +R [ <. b , 1P >. ] ~R ) -> ( y <R z <-> y <R ( C +R [ <. b , 1P >. ] ~R ) ) )
9594rspcev 2793 . . . . . . . . . . . 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 2557 . . . . . . . . . 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 2576 . . . . . . . . 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 488 . . . . . . . . . 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 3941 . . . . . . . . . . 11 |- ( z = C -> ( y <R z <-> y <R C ) )
104103rspcev 2793 . . . . . . . . . 10 |- ( ( C e. A /\ y <R C ) -> E. z e. A y <R z )
105102, 104sylancom 417 . . . . . . . . 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 7609 . . . . . . . . . . . 12 |- ( C e. R. -> ( C +R -1R ) <R C )
1078, 106syl 14 . . . . . . . . . . 11 |- ( ph -> ( C +R -1R ) <R C )
108107ad4antr 486 . . . . . . . . . 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 484 . . . . . . . . . . . 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 7584 . . . . . . . . . . . 12 |- -1R e. R.
111 addclsr 7585 . . . . . . . . . . . 12 |- ( ( C e. R. /\ -1R e. R. ) -> ( C +R -1R ) e. R. )
112109, 110, 111sylancl 410 . . . . . . . . . . 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 520 . . . . . . . . . . 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 4250 . . . . . . . . . . . 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 421 . . . . . . . . . . 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 1217 . . . . . . . . . 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 788 . . . . . . . 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 2508 . . . . . 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 3940 . . . . . . . 8 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( x <R y <-> ( C +R [ <. v , 1P >. ] ~R ) <R y ) )
124123notbid 657 . . . . . . 7 |- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( -. x <R y <-> -. ( C +R [ <. v , 1P >. ] ~R ) <R y ) )
125124ralbidv 2438 . . . . . 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 3941 . . . . . . . 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 2438 . . . . . 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 465 . . . . 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 2793 . . . 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 1411 . . 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 2552 . 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 698   /\ w3a 963   = wceq 1332   F. wfal 1337   e. wcel 1481   A.wral 2417   E.wrex 2418   {crab 2421   C_ wss 3076   <.cop 3535   class class class wbr 3937   Or wor 4225  (class class class)co 5782   [cec 6435   P.cnp 7123   1Pc1p 7124   <P cltp 7127   ~R cer 7128   R.cnr 7129   -1Rcm1r 7132   +R cplr 7133   <R cltr 7135
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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4051  ax-sep 4054  ax-nul 4062  ax-pow 4106  ax-pr 4139  ax-un 4363  ax-setind 4460  ax-iinf 4510
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2914  df-csb 3008  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-nul 3369  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-int 3780  df-iun 3823  df-br 3938  df-opab 3998  df-mpt 3999  df-tr 4035  df-eprel 4219  df-id 4223  df-po 4226  df-iso 4227  df-iord 4296  df-on 4298  df-suc 4301  df-iom 4513  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-rn 4558  df-res 4559  df-ima 4560  df-iota 5096  df-fun 5133  df-fn 5134  df-f 5135  df-f1 5136  df-fo 5137  df-f1o 5138  df-fv 5139  df-ov 5785  df-oprab 5786  df-mpo 5787  df-1st 6046  df-2nd 6047  df-recs 6210  df-irdg 6275  df-1o 6321  df-2o 6322  df-oadd 6325  df-omul 6326  df-er 6437  df-ec 6439  df-qs 6443  df-ni 7136  df-pli 7137  df-mi 7138  df-lti 7139  df-plpq 7176  df-mpq 7177  df-enq 7179  df-nqqs 7180  df-plqqs 7181  df-mqqs 7182  df-1nqqs 7183  df-rq 7184  df-ltnqqs 7185  df-enq0 7256  df-nq0 7257  df-0nq0 7258  df-plq0 7259  df-mq0 7260  df-inp 7298  df-i1p 7299  df-iplp 7300  df-imp 7301  df-iltp 7302  df-enr 7558  df-nr 7559  df-plr 7560  df-mr 7561  df-ltr 7562  df-0r 7563  df-1r 7564  df-m1r 7565
This theorem is referenced by:  suplocsr  7641
  Copyright terms: Public domain W3C validator