MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  supsrlem Structured version   Visualization version   GIF version

Theorem supsrlem 10095
Description: Lemma for supremum theorem. (Contributed by NM, 21-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
supsrlem.1 𝐵 = {𝑤 ∣ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴}
supsrlem.2 𝐶R
Assertion
Ref Expression
supsrlem ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧)))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑤,𝐴   𝑥,𝐵,𝑦,𝑧,𝑤   𝑥,𝐶,𝑦,𝑧,𝑤

Proof of Theorem supsrlem
Dummy variables 𝑣 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 supsrlem.2 . . . . . . 7 𝐶R
2 0idsr 10081 . . . . . . 7 (𝐶R → (𝐶 +R 0R) = 𝐶)
31, 2mp1i 13 . . . . . 6 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → (𝐶 +R 0R) = 𝐶)
4 simpl 474 . . . . . 6 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → 𝐶𝐴)
53, 4eqeltrd 2827 . . . . 5 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → (𝐶 +R 0R) ∈ 𝐴)
6 1pr 10000 . . . . . . 7 1PP
76elexi 3341 . . . . . 6 1P ∈ V
8 opeq1 4541 . . . . . . . . . 10 (𝑤 = 1P → ⟨𝑤, 1P⟩ = ⟨1P, 1P⟩)
98eceq1d 7938 . . . . . . . . 9 (𝑤 = 1P → [⟨𝑤, 1P⟩] ~R = [⟨1P, 1P⟩] ~R )
10 df-0r 10045 . . . . . . . . 9 0R = [⟨1P, 1P⟩] ~R
119, 10syl6eqr 2800 . . . . . . . 8 (𝑤 = 1P → [⟨𝑤, 1P⟩] ~R = 0R)
1211oveq2d 6817 . . . . . . 7 (𝑤 = 1P → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = (𝐶 +R 0R))
1312eleq1d 2812 . . . . . 6 (𝑤 = 1P → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴 ↔ (𝐶 +R 0R) ∈ 𝐴))
14 supsrlem.1 . . . . . 6 𝐵 = {𝑤 ∣ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴}
157, 13, 14elab2 3482 . . . . 5 (1P𝐵 ↔ (𝐶 +R 0R) ∈ 𝐴)
165, 15sylibr 224 . . . 4 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → 1P𝐵)
17 ne0i 4052 . . . 4 (1P𝐵𝐵 ≠ ∅)
1816, 17syl 17 . . 3 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → 𝐵 ≠ ∅)
19 breq1 4795 . . . . . . . 8 (𝑦 = 𝐶 → (𝑦 <R 𝑥𝐶 <R 𝑥))
2019rspccv 3434 . . . . . . 7 (∀𝑦𝐴 𝑦 <R 𝑥 → (𝐶𝐴𝐶 <R 𝑥))
21 0lt1sr 10079 . . . . . . . . . . . . 13 0R <R 1R
22 m1r 10066 . . . . . . . . . . . . . 14 -1RR
23 ltasr 10084 . . . . . . . . . . . . . 14 (-1RR → (0R <R 1R ↔ (-1R +R 0R) <R (-1R +R 1R)))
2422, 23ax-mp 5 . . . . . . . . . . . . 13 (0R <R 1R ↔ (-1R +R 0R) <R (-1R +R 1R))
2521, 24mpbi 220 . . . . . . . . . . . 12 (-1R +R 0R) <R (-1R +R 1R)
26 0idsr 10081 . . . . . . . . . . . . 13 (-1RR → (-1R +R 0R) = -1R)
2722, 26ax-mp 5 . . . . . . . . . . . 12 (-1R +R 0R) = -1R
28 m1p1sr 10076 . . . . . . . . . . . 12 (-1R +R 1R) = 0R
2925, 27, 283brtr3i 4821 . . . . . . . . . . 11 -1R <R 0R
30 ltasr 10084 . . . . . . . . . . . 12 (𝐶R → (-1R <R 0R ↔ (𝐶 +R -1R) <R (𝐶 +R 0R)))
311, 30ax-mp 5 . . . . . . . . . . 11 (-1R <R 0R ↔ (𝐶 +R -1R) <R (𝐶 +R 0R))
3229, 31mpbi 220 . . . . . . . . . 10 (𝐶 +R -1R) <R (𝐶 +R 0R)
331, 2ax-mp 5 . . . . . . . . . 10 (𝐶 +R 0R) = 𝐶
3432, 33breqtri 4817 . . . . . . . . 9 (𝐶 +R -1R) <R 𝐶
35 ltsosr 10078 . . . . . . . . . 10 <R Or R
36 ltrelsr 10052 . . . . . . . . . 10 <R ⊆ (R × R)
3735, 36sotri 5669 . . . . . . . . 9 (((𝐶 +R -1R) <R 𝐶𝐶 <R 𝑥) → (𝐶 +R -1R) <R 𝑥)
3834, 37mpan 708 . . . . . . . 8 (𝐶 <R 𝑥 → (𝐶 +R -1R) <R 𝑥)
391map2psrpr 10094 . . . . . . . 8 ((𝐶 +R -1R) <R 𝑥 ↔ ∃𝑣P (𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥)
4038, 39sylib 208 . . . . . . 7 (𝐶 <R 𝑥 → ∃𝑣P (𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥)
4120, 40syl6 35 . . . . . 6 (∀𝑦𝐴 𝑦 <R 𝑥 → (𝐶𝐴 → ∃𝑣P (𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥))
42 breq2 4796 . . . . . . . . . 10 ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥 → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑦 <R 𝑥))
4342ralbidv 3112 . . . . . . . . 9 ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥 → (∀𝑦𝐴 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ ∀𝑦𝐴 𝑦 <R 𝑥))
4414abeq2i 2861 . . . . . . . . . . 11 (𝑤𝐵 ↔ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴)
45 breq1 4795 . . . . . . . . . . . . 13 (𝑦 = (𝐶 +R [⟨𝑤, 1P⟩] ~R ) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )))
4645rspccv 3434 . . . . . . . . . . . 12 (∀𝑦𝐴 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴 → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )))
471ltpsrpr 10093 . . . . . . . . . . . 12 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑤<P 𝑣)
4846, 47syl6ib 241 . . . . . . . . . . 11 (∀𝑦𝐴 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴𝑤<P 𝑣))
4944, 48syl5bi 232 . . . . . . . . . 10 (∀𝑦𝐴 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑤𝐵𝑤<P 𝑣))
5049ralrimiv 3091 . . . . . . . . 9 (∀𝑦𝐴 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∀𝑤𝐵 𝑤<P 𝑣)
5143, 50syl6bir 244 . . . . . . . 8 ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥 → (∀𝑦𝐴 𝑦 <R 𝑥 → ∀𝑤𝐵 𝑤<P 𝑣))
5251com12 32 . . . . . . 7 (∀𝑦𝐴 𝑦 <R 𝑥 → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥 → ∀𝑤𝐵 𝑤<P 𝑣))
5352reximdv 3142 . . . . . 6 (∀𝑦𝐴 𝑦 <R 𝑥 → (∃𝑣P (𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥 → ∃𝑣P𝑤𝐵 𝑤<P 𝑣))
5441, 53syld 47 . . . . 5 (∀𝑦𝐴 𝑦 <R 𝑥 → (𝐶𝐴 → ∃𝑣P𝑤𝐵 𝑤<P 𝑣))
5554rexlimivw 3155 . . . 4 (∃𝑥R𝑦𝐴 𝑦 <R 𝑥 → (𝐶𝐴 → ∃𝑣P𝑤𝐵 𝑤<P 𝑣))
5655impcom 445 . . 3 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → ∃𝑣P𝑤𝐵 𝑤<P 𝑣)
57 supexpr 10039 . . 3 ((𝐵 ≠ ∅ ∧ ∃𝑣P𝑤𝐵 𝑤<P 𝑣) → ∃𝑣P (∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)))
5818, 56, 57syl2anc 696 . 2 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → ∃𝑣P (∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)))
591mappsrpr 10092 . . . . . . 7 ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑣P)
6036brel 5313 . . . . . . 7 ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((𝐶 +R -1R) ∈ R ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R))
6159, 60sylbir 225 . . . . . 6 (𝑣P → ((𝐶 +R -1R) ∈ R ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R))
6261simprd 482 . . . . 5 (𝑣P → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R)
6362adantl 473 . . . 4 (((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) ∧ 𝑣P) → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R)
6435, 36sotri 5669 . . . . . . . . . . . . . . 15 (((𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → (𝐶 +R -1R) <R 𝑦)
6559, 64sylanbr 491 . . . . . . . . . . . . . 14 ((𝑣P ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → (𝐶 +R -1R) <R 𝑦)
661map2psrpr 10094 . . . . . . . . . . . . . 14 ((𝐶 +R -1R) <R 𝑦 ↔ ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
6765, 66sylib 208 . . . . . . . . . . . . 13 ((𝑣P ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
68 rexex 3128 . . . . . . . . . . . . 13 (∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ∃𝑤(𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
69 df-ral 3043 . . . . . . . . . . . . . . 15 (∀𝑤𝐵 ¬ 𝑣<P 𝑤 ↔ ∀𝑤(𝑤𝐵 → ¬ 𝑣<P 𝑤))
70 19.29 1938 . . . . . . . . . . . . . . . 16 ((∀𝑤(𝑤𝐵 → ¬ 𝑣<P 𝑤) ∧ ∃𝑤(𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∃𝑤((𝑤𝐵 → ¬ 𝑣<P 𝑤) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦))
71 eleq1 2815 . . . . . . . . . . . . . . . . . . . 20 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴𝑦𝐴))
7244, 71syl5bb 272 . . . . . . . . . . . . . . . . . . 19 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (𝑤𝐵𝑦𝐴))
731ltpsrpr 10093 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ↔ 𝑣<P 𝑤)
74 breq2 4796 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ↔ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
7573, 74syl5bbr 274 . . . . . . . . . . . . . . . . . . . 20 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (𝑣<P 𝑤 ↔ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
7675notbid 307 . . . . . . . . . . . . . . . . . . 19 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (¬ 𝑣<P 𝑤 ↔ ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
7772, 76imbi12d 333 . . . . . . . . . . . . . . . . . 18 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ((𝑤𝐵 → ¬ 𝑣<P 𝑤) ↔ (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)))
7877biimpac 504 . . . . . . . . . . . . . . . . 17 (((𝑤𝐵 → ¬ 𝑣<P 𝑤) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
7978exlimiv 1995 . . . . . . . . . . . . . . . 16 (∃𝑤((𝑤𝐵 → ¬ 𝑣<P 𝑤) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
8070, 79syl 17 . . . . . . . . . . . . . . 15 ((∀𝑤(𝑤𝐵 → ¬ 𝑣<P 𝑤) ∧ ∃𝑤(𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
8169, 80sylanb 490 . . . . . . . . . . . . . 14 ((∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∃𝑤(𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
8281expcom 450 . . . . . . . . . . . . 13 (∃𝑤(𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (∀𝑤𝐵 ¬ 𝑣<P 𝑤 → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)))
8367, 68, 823syl 18 . . . . . . . . . . . 12 ((𝑣P ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → (∀𝑤𝐵 ¬ 𝑣<P 𝑤 → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)))
8483impd 446 . . . . . . . . . . 11 ((𝑣P ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ((∀𝑤𝐵 ¬ 𝑣<P 𝑤𝑦𝐴) → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
8584impancom 455 . . . . . . . . . 10 ((𝑣P ∧ (∀𝑤𝐵 ¬ 𝑣<P 𝑤𝑦𝐴)) → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
8685pm2.01d 181 . . . . . . . . 9 ((𝑣P ∧ (∀𝑤𝐵 ¬ 𝑣<P 𝑤𝑦𝐴)) → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
8786expr 644 . . . . . . . 8 ((𝑣P ∧ ∀𝑤𝐵 ¬ 𝑣<P 𝑤) → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
8887ralrimiv 3091 . . . . . . 7 ((𝑣P ∧ ∀𝑤𝐵 ¬ 𝑣<P 𝑤) → ∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
8988ex 449 . . . . . 6 (𝑣P → (∀𝑤𝐵 ¬ 𝑣<P 𝑤 → ∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
9089adantl 473 . . . . 5 (((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) ∧ 𝑣P) → (∀𝑤𝐵 ¬ 𝑣<P 𝑤 → ∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
91 r19.29 3198 . . . . . . . . . . . . . 14 ((∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) ∧ ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∃𝑤P ((𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦))
92 breq1 4795 . . . . . . . . . . . . . . . . . . 19 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )))
9347, 92syl5bbr 274 . . . . . . . . . . . . . . . . . 18 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (𝑤<P 𝑣𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )))
9493biimprd 238 . . . . . . . . . . . . . . . . 17 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → 𝑤<P 𝑣))
95 vex 3331 . . . . . . . . . . . . . . . . . . . . 21 𝑢 ∈ V
96 opeq1 4541 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑢 → ⟨𝑤, 1P⟩ = ⟨𝑢, 1P⟩)
9796eceq1d 7938 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑢 → [⟨𝑤, 1P⟩] ~R = [⟨𝑢, 1P⟩] ~R )
9897oveq2d 6817 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑢 → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = (𝐶 +R [⟨𝑢, 1P⟩] ~R ))
9998eleq1d 2812 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑢 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴 ↔ (𝐶 +R [⟨𝑢, 1P⟩] ~R ) ∈ 𝐴))
10095, 99, 14elab2 3482 . . . . . . . . . . . . . . . . . . . 20 (𝑢𝐵 ↔ (𝐶 +R [⟨𝑢, 1P⟩] ~R ) ∈ 𝐴)
101 breq2 4796 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (𝐶 +R [⟨𝑢, 1P⟩] ~R ) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧 ↔ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑢, 1P⟩] ~R )))
1021ltpsrpr 10093 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑢, 1P⟩] ~R ) ↔ 𝑤<P 𝑢)
103101, 102syl6bb 276 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = (𝐶 +R [⟨𝑢, 1P⟩] ~R ) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧𝑤<P 𝑢))
104103rspcev 3437 . . . . . . . . . . . . . . . . . . . 20 (((𝐶 +R [⟨𝑢, 1P⟩] ~R ) ∈ 𝐴𝑤<P 𝑢) → ∃𝑧𝐴 (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧)
105100, 104sylanb 490 . . . . . . . . . . . . . . . . . . 19 ((𝑢𝐵𝑤<P 𝑢) → ∃𝑧𝐴 (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧)
106105rexlimiva 3154 . . . . . . . . . . . . . . . . . 18 (∃𝑢𝐵 𝑤<P 𝑢 → ∃𝑧𝐴 (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧)
107 breq1 4795 . . . . . . . . . . . . . . . . . . 19 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧𝑦 <R 𝑧))
108107rexbidv 3178 . . . . . . . . . . . . . . . . . 18 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (∃𝑧𝐴 (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧 ↔ ∃𝑧𝐴 𝑦 <R 𝑧))
109106, 108syl5ib 234 . . . . . . . . . . . . . . . . 17 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (∃𝑢𝐵 𝑤<P 𝑢 → ∃𝑧𝐴 𝑦 <R 𝑧))
11094, 109imim12d 81 . . . . . . . . . . . . . . . 16 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ((𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
111110impcom 445 . . . . . . . . . . . . . . 15 (((𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))
112111rexlimivw 3155 . . . . . . . . . . . . . 14 (∃𝑤P ((𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))
11391, 112syl 17 . . . . . . . . . . . . 13 ((∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) ∧ ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))
11466, 113sylan2b 493 . . . . . . . . . . . 12 ((∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) ∧ (𝐶 +R -1R) <R 𝑦) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))
115114ex 449 . . . . . . . . . . 11 (∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) → ((𝐶 +R -1R) <R 𝑦 → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
116115adantl 473 . . . . . . . . . 10 (((𝐶𝐴𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → ((𝐶 +R -1R) <R 𝑦 → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
117116a1dd 50 . . . . . . . . 9 (((𝐶𝐴𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → ((𝐶 +R -1R) <R 𝑦 → (𝑦R → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))))
11835, 36sotri2 5671 . . . . . . . . . . . . 13 ((𝑦R ∧ ¬ (𝐶 +R -1R) <R 𝑦 ∧ (𝐶 +R -1R) <R 𝐶) → 𝑦 <R 𝐶)
11934, 118mp3an3 1550 . . . . . . . . . . . 12 ((𝑦R ∧ ¬ (𝐶 +R -1R) <R 𝑦) → 𝑦 <R 𝐶)
120 breq2 4796 . . . . . . . . . . . . . . 15 (𝑧 = 𝐶 → (𝑦 <R 𝑧𝑦 <R 𝐶))
121120rspcev 3437 . . . . . . . . . . . . . 14 ((𝐶𝐴𝑦 <R 𝐶) → ∃𝑧𝐴 𝑦 <R 𝑧)
122121ex 449 . . . . . . . . . . . . 13 (𝐶𝐴 → (𝑦 <R 𝐶 → ∃𝑧𝐴 𝑦 <R 𝑧))
123122a1dd 50 . . . . . . . . . . . 12 (𝐶𝐴 → (𝑦 <R 𝐶 → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
124119, 123syl5 34 . . . . . . . . . . 11 (𝐶𝐴 → ((𝑦R ∧ ¬ (𝐶 +R -1R) <R 𝑦) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
125124expcomd 453 . . . . . . . . . 10 (𝐶𝐴 → (¬ (𝐶 +R -1R) <R 𝑦 → (𝑦R → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))))
126125ad2antrr 764 . . . . . . . . 9 (((𝐶𝐴𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → (¬ (𝐶 +R -1R) <R 𝑦 → (𝑦R → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))))
127117, 126pm2.61d 170 . . . . . . . 8 (((𝐶𝐴𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → (𝑦R → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
128127ralrimiv 3091 . . . . . . 7 (((𝐶𝐴𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))
129128ex 449 . . . . . 6 ((𝐶𝐴𝑣P) → (∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) → ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
130129adantlr 753 . . . . 5 (((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) ∧ 𝑣P) → (∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) → ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
13190, 130anim12d 587 . . . 4 (((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) ∧ 𝑣P) → ((∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → (∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))))
132 breq1 4795 . . . . . . . 8 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑥 <R 𝑦 ↔ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
133132notbid 307 . . . . . . 7 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (¬ 𝑥 <R 𝑦 ↔ ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
134133ralbidv 3112 . . . . . 6 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ↔ ∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
135 breq2 4796 . . . . . . . 8 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑦 <R 𝑥𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )))
136135imbi1d 330 . . . . . . 7 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧) ↔ (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
137136ralbidv 3112 . . . . . 6 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧) ↔ ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
138134, 137anbi12d 749 . . . . 5 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧)) ↔ (∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))))
139138rspcev 3437 . . . 4 (((𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R ∧ (∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧)))
14063, 131, 139syl6an 569 . . 3 (((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) ∧ 𝑣P) → ((∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧))))
141140rexlimdva 3157 . 2 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → (∃𝑣P (∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧))))
14258, 141mpd 15 1 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  wal 1618   = wceq 1620  wex 1841  wcel 2127  {cab 2734  wne 2920  wral 3038  wrex 3039  c0 4046  cop 4315   class class class wbr 4792  (class class class)co 6801  [cec 7897  Pcnp 9844  1Pc1p 9845  <P cltp 9848   ~R cer 9849  Rcnr 9850  0Rc0r 9851  1Rc1r 9852  -1Rcm1r 9853   +R cplr 9854   <R cltr 9856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-inf2 8699
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-reu 3045  df-rmo 3046  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-int 4616  df-iun 4662  df-br 4793  df-opab 4853  df-mpt 4870  df-tr 4893  df-id 5162  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-we 5215  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-pred 5829  df-ord 5875  df-on 5876  df-lim 5877  df-suc 5878  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-om 7219  df-1st 7321  df-2nd 7322  df-wrecs 7564  df-recs 7625  df-rdg 7663  df-1o 7717  df-oadd 7721  df-omul 7722  df-er 7899  df-ec 7901  df-qs 7905  df-ni 9857  df-pli 9858  df-mi 9859  df-lti 9860  df-plpq 9893  df-mpq 9894  df-ltpq 9895  df-enq 9896  df-nq 9897  df-erq 9898  df-plq 9899  df-mq 9900  df-1nq 9901  df-rq 9902  df-ltnq 9903  df-np 9966  df-1p 9967  df-plp 9968  df-mp 9969  df-ltp 9970  df-enr 10040  df-nr 10041  df-plr 10042  df-mr 10043  df-ltr 10044  df-0r 10045  df-1r 10046  df-m1r 10047
This theorem is referenced by:  supsr  10096
  Copyright terms: Public domain W3C validator