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

Theorem supsrlem 10521
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 10507 . . . . . . 7 (𝐶R → (𝐶 +R 0R) = 𝐶)
31, 2mp1i 13 . . . . . 6 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → (𝐶 +R 0R) = 𝐶)
4 simpl 483 . . . . . 6 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → 𝐶𝐴)
53, 4eqeltrd 2910 . . . . 5 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → (𝐶 +R 0R) ∈ 𝐴)
6 1pr 10425 . . . . . . 7 1PP
76elexi 3511 . . . . . 6 1P ∈ V
8 opeq1 4795 . . . . . . . . . 10 (𝑤 = 1P → ⟨𝑤, 1P⟩ = ⟨1P, 1P⟩)
98eceq1d 8317 . . . . . . . . 9 (𝑤 = 1P → [⟨𝑤, 1P⟩] ~R = [⟨1P, 1P⟩] ~R )
10 df-0r 10470 . . . . . . . . 9 0R = [⟨1P, 1P⟩] ~R
119, 10syl6eqr 2871 . . . . . . . 8 (𝑤 = 1P → [⟨𝑤, 1P⟩] ~R = 0R)
1211oveq2d 7161 . . . . . . 7 (𝑤 = 1P → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = (𝐶 +R 0R))
1312eleq1d 2894 . . . . . 6 (𝑤 = 1P → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴 ↔ (𝐶 +R 0R) ∈ 𝐴))
14 supsrlem.1 . . . . . 6 𝐵 = {𝑤 ∣ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴}
157, 13, 14elab2 3667 . . . . 5 (1P𝐵 ↔ (𝐶 +R 0R) ∈ 𝐴)
165, 15sylibr 235 . . . 4 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → 1P𝐵)
1716ne0d 4298 . . 3 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → 𝐵 ≠ ∅)
18 breq1 5060 . . . . . . . 8 (𝑦 = 𝐶 → (𝑦 <R 𝑥𝐶 <R 𝑥))
1918rspccv 3617 . . . . . . 7 (∀𝑦𝐴 𝑦 <R 𝑥 → (𝐶𝐴𝐶 <R 𝑥))
20 0lt1sr 10505 . . . . . . . . . . . . 13 0R <R 1R
21 m1r 10492 . . . . . . . . . . . . . 14 -1RR
22 ltasr 10510 . . . . . . . . . . . . . 14 (-1RR → (0R <R 1R ↔ (-1R +R 0R) <R (-1R +R 1R)))
2321, 22ax-mp 5 . . . . . . . . . . . . 13 (0R <R 1R ↔ (-1R +R 0R) <R (-1R +R 1R))
2420, 23mpbi 231 . . . . . . . . . . . 12 (-1R +R 0R) <R (-1R +R 1R)
25 0idsr 10507 . . . . . . . . . . . . 13 (-1RR → (-1R +R 0R) = -1R)
2621, 25ax-mp 5 . . . . . . . . . . . 12 (-1R +R 0R) = -1R
27 m1p1sr 10502 . . . . . . . . . . . 12 (-1R +R 1R) = 0R
2824, 26, 273brtr3i 5086 . . . . . . . . . . 11 -1R <R 0R
29 ltasr 10510 . . . . . . . . . . . 12 (𝐶R → (-1R <R 0R ↔ (𝐶 +R -1R) <R (𝐶 +R 0R)))
301, 29ax-mp 5 . . . . . . . . . . 11 (-1R <R 0R ↔ (𝐶 +R -1R) <R (𝐶 +R 0R))
3128, 30mpbi 231 . . . . . . . . . 10 (𝐶 +R -1R) <R (𝐶 +R 0R)
321, 2ax-mp 5 . . . . . . . . . 10 (𝐶 +R 0R) = 𝐶
3331, 32breqtri 5082 . . . . . . . . 9 (𝐶 +R -1R) <R 𝐶
34 ltsosr 10504 . . . . . . . . . 10 <R Or R
35 ltrelsr 10478 . . . . . . . . . 10 <R ⊆ (R × R)
3634, 35sotri 5980 . . . . . . . . 9 (((𝐶 +R -1R) <R 𝐶𝐶 <R 𝑥) → (𝐶 +R -1R) <R 𝑥)
3733, 36mpan 686 . . . . . . . 8 (𝐶 <R 𝑥 → (𝐶 +R -1R) <R 𝑥)
381map2psrpr 10520 . . . . . . . 8 ((𝐶 +R -1R) <R 𝑥 ↔ ∃𝑣P (𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥)
3937, 38sylib 219 . . . . . . 7 (𝐶 <R 𝑥 → ∃𝑣P (𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥)
4019, 39syl6 35 . . . . . 6 (∀𝑦𝐴 𝑦 <R 𝑥 → (𝐶𝐴 → ∃𝑣P (𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥))
41 breq2 5061 . . . . . . . . . 10 ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥 → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑦 <R 𝑥))
4241ralbidv 3194 . . . . . . . . 9 ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥 → (∀𝑦𝐴 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ ∀𝑦𝐴 𝑦 <R 𝑥))
4314abeq2i 2945 . . . . . . . . . . 11 (𝑤𝐵 ↔ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴)
44 breq1 5060 . . . . . . . . . . . . 13 (𝑦 = (𝐶 +R [⟨𝑤, 1P⟩] ~R ) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )))
4544rspccv 3617 . . . . . . . . . . . 12 (∀𝑦𝐴 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴 → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )))
461ltpsrpr 10519 . . . . . . . . . . . 12 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑤<P 𝑣)
4745, 46syl6ib 252 . . . . . . . . . . 11 (∀𝑦𝐴 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴𝑤<P 𝑣))
4843, 47syl5bi 243 . . . . . . . . . 10 (∀𝑦𝐴 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑤𝐵𝑤<P 𝑣))
4948ralrimiv 3178 . . . . . . . . 9 (∀𝑦𝐴 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∀𝑤𝐵 𝑤<P 𝑣)
5042, 49syl6bir 255 . . . . . . . 8 ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥 → (∀𝑦𝐴 𝑦 <R 𝑥 → ∀𝑤𝐵 𝑤<P 𝑣))
5150com12 32 . . . . . . 7 (∀𝑦𝐴 𝑦 <R 𝑥 → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥 → ∀𝑤𝐵 𝑤<P 𝑣))
5251reximdv 3270 . . . . . 6 (∀𝑦𝐴 𝑦 <R 𝑥 → (∃𝑣P (𝐶 +R [⟨𝑣, 1P⟩] ~R ) = 𝑥 → ∃𝑣P𝑤𝐵 𝑤<P 𝑣))
5340, 52syld 47 . . . . 5 (∀𝑦𝐴 𝑦 <R 𝑥 → (𝐶𝐴 → ∃𝑣P𝑤𝐵 𝑤<P 𝑣))
5453rexlimivw 3279 . . . 4 (∃𝑥R𝑦𝐴 𝑦 <R 𝑥 → (𝐶𝐴 → ∃𝑣P𝑤𝐵 𝑤<P 𝑣))
5554impcom 408 . . 3 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → ∃𝑣P𝑤𝐵 𝑤<P 𝑣)
56 supexpr 10464 . . 3 ((𝐵 ≠ ∅ ∧ ∃𝑣P𝑤𝐵 𝑤<P 𝑣) → ∃𝑣P (∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)))
5717, 55, 56syl2anc 584 . 2 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → ∃𝑣P (∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)))
581mappsrpr 10518 . . . . . . 7 ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑣P)
5935brel 5610 . . . . . . 7 ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((𝐶 +R -1R) ∈ R ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R))
6058, 59sylbir 236 . . . . . 6 (𝑣P → ((𝐶 +R -1R) ∈ R ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R))
6160simprd 496 . . . . 5 (𝑣P → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R)
6261adantl 482 . . . 4 (((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) ∧ 𝑣P) → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R)
6334, 35sotri 5980 . . . . . . . . . . . . . . 15 (((𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → (𝐶 +R -1R) <R 𝑦)
6458, 63sylanbr 582 . . . . . . . . . . . . . 14 ((𝑣P ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → (𝐶 +R -1R) <R 𝑦)
651map2psrpr 10520 . . . . . . . . . . . . . 14 ((𝐶 +R -1R) <R 𝑦 ↔ ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
6664, 65sylib 219 . . . . . . . . . . . . 13 ((𝑣P ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
67 rexex 3237 . . . . . . . . . . . . 13 (∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ∃𝑤(𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
68 df-ral 3140 . . . . . . . . . . . . . . 15 (∀𝑤𝐵 ¬ 𝑣<P 𝑤 ↔ ∀𝑤(𝑤𝐵 → ¬ 𝑣<P 𝑤))
69 19.29 1865 . . . . . . . . . . . . . . . 16 ((∀𝑤(𝑤𝐵 → ¬ 𝑣<P 𝑤) ∧ ∃𝑤(𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∃𝑤((𝑤𝐵 → ¬ 𝑣<P 𝑤) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦))
70 eleq1 2897 . . . . . . . . . . . . . . . . . . . 20 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴𝑦𝐴))
7143, 70syl5bb 284 . . . . . . . . . . . . . . . . . . 19 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (𝑤𝐵𝑦𝐴))
721ltpsrpr 10519 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ↔ 𝑣<P 𝑤)
73 breq2 5061 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ↔ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
7472, 73syl5bbr 286 . . . . . . . . . . . . . . . . . . . 20 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (𝑣<P 𝑤 ↔ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
7574notbid 319 . . . . . . . . . . . . . . . . . . 19 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (¬ 𝑣<P 𝑤 ↔ ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
7671, 75imbi12d 346 . . . . . . . . . . . . . . . . . 18 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ((𝑤𝐵 → ¬ 𝑣<P 𝑤) ↔ (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)))
7776biimpac 479 . . . . . . . . . . . . . . . . 17 (((𝑤𝐵 → ¬ 𝑣<P 𝑤) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
7877exlimiv 1922 . . . . . . . . . . . . . . . 16 (∃𝑤((𝑤𝐵 → ¬ 𝑣<P 𝑤) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
7969, 78syl 17 . . . . . . . . . . . . . . 15 ((∀𝑤(𝑤𝐵 → ¬ 𝑣<P 𝑤) ∧ ∃𝑤(𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
8068, 79sylanb 581 . . . . . . . . . . . . . 14 ((∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∃𝑤(𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
8180expcom 414 . . . . . . . . . . . . 13 (∃𝑤(𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (∀𝑤𝐵 ¬ 𝑣<P 𝑤 → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)))
8266, 67, 813syl 18 . . . . . . . . . . . 12 ((𝑣P ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → (∀𝑤𝐵 ¬ 𝑣<P 𝑤 → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)))
8382impd 411 . . . . . . . . . . 11 ((𝑣P ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ((∀𝑤𝐵 ¬ 𝑣<P 𝑤𝑦𝐴) → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
8483impancom 452 . . . . . . . . . 10 ((𝑣P ∧ (∀𝑤𝐵 ¬ 𝑣<P 𝑤𝑦𝐴)) → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
8584pm2.01d 191 . . . . . . . . 9 ((𝑣P ∧ (∀𝑤𝐵 ¬ 𝑣<P 𝑤𝑦𝐴)) → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
8685expr 457 . . . . . . . 8 ((𝑣P ∧ ∀𝑤𝐵 ¬ 𝑣<P 𝑤) → (𝑦𝐴 → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
8786ralrimiv 3178 . . . . . . 7 ((𝑣P ∧ ∀𝑤𝐵 ¬ 𝑣<P 𝑤) → ∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
8887ex 413 . . . . . 6 (𝑣P → (∀𝑤𝐵 ¬ 𝑣<P 𝑤 → ∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
8988adantl 482 . . . . 5 (((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) ∧ 𝑣P) → (∀𝑤𝐵 ¬ 𝑣<P 𝑤 → ∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
90 r19.29 3251 . . . . . . . . . . . . . 14 ((∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) ∧ ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∃𝑤P ((𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦))
91 breq1 5060 . . . . . . . . . . . . . . . . . . 19 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )))
9246, 91syl5bbr 286 . . . . . . . . . . . . . . . . . 18 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (𝑤<P 𝑣𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )))
9392biimprd 249 . . . . . . . . . . . . . . . . 17 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → 𝑤<P 𝑣))
94 vex 3495 . . . . . . . . . . . . . . . . . . . . 21 𝑢 ∈ V
95 opeq1 4795 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑢 → ⟨𝑤, 1P⟩ = ⟨𝑢, 1P⟩)
9695eceq1d 8317 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑢 → [⟨𝑤, 1P⟩] ~R = [⟨𝑢, 1P⟩] ~R )
9796oveq2d 7161 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑢 → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = (𝐶 +R [⟨𝑢, 1P⟩] ~R ))
9897eleq1d 2894 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑢 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴 ↔ (𝐶 +R [⟨𝑢, 1P⟩] ~R ) ∈ 𝐴))
9994, 98, 14elab2 3667 . . . . . . . . . . . . . . . . . . . 20 (𝑢𝐵 ↔ (𝐶 +R [⟨𝑢, 1P⟩] ~R ) ∈ 𝐴)
100 breq2 5061 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (𝐶 +R [⟨𝑢, 1P⟩] ~R ) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧 ↔ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑢, 1P⟩] ~R )))
1011ltpsrpr 10519 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑢, 1P⟩] ~R ) ↔ 𝑤<P 𝑢)
102100, 101syl6bb 288 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = (𝐶 +R [⟨𝑢, 1P⟩] ~R ) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧𝑤<P 𝑢))
103102rspcev 3620 . . . . . . . . . . . . . . . . . . . 20 (((𝐶 +R [⟨𝑢, 1P⟩] ~R ) ∈ 𝐴𝑤<P 𝑢) → ∃𝑧𝐴 (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧)
10499, 103sylanb 581 . . . . . . . . . . . . . . . . . . 19 ((𝑢𝐵𝑤<P 𝑢) → ∃𝑧𝐴 (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧)
105104rexlimiva 3278 . . . . . . . . . . . . . . . . . 18 (∃𝑢𝐵 𝑤<P 𝑢 → ∃𝑧𝐴 (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧)
106 breq1 5060 . . . . . . . . . . . . . . . . . . 19 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧𝑦 <R 𝑧))
107106rexbidv 3294 . . . . . . . . . . . . . . . . . 18 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (∃𝑧𝐴 (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R 𝑧 ↔ ∃𝑧𝐴 𝑦 <R 𝑧))
108105, 107syl5ib 245 . . . . . . . . . . . . . . . . 17 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → (∃𝑢𝐵 𝑤<P 𝑢 → ∃𝑧𝐴 𝑦 <R 𝑧))
10993, 108imim12d 81 . . . . . . . . . . . . . . . 16 ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦 → ((𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
110109impcom 408 . . . . . . . . . . . . . . 15 (((𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))
111110rexlimivw 3279 . . . . . . . . . . . . . 14 (∃𝑤P ((𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))
11290, 111syl 17 . . . . . . . . . . . . 13 ((∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) ∧ ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))
11365, 112sylan2b 593 . . . . . . . . . . . 12 ((∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) ∧ (𝐶 +R -1R) <R 𝑦) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))
114113ex 413 . . . . . . . . . . 11 (∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) → ((𝐶 +R -1R) <R 𝑦 → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
115114adantl 482 . . . . . . . . . 10 (((𝐶𝐴𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → ((𝐶 +R -1R) <R 𝑦 → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
116115a1dd 50 . . . . . . . . 9 (((𝐶𝐴𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → ((𝐶 +R -1R) <R 𝑦 → (𝑦R → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))))
11734, 35sotri2 5982 . . . . . . . . . . . . 13 ((𝑦R ∧ ¬ (𝐶 +R -1R) <R 𝑦 ∧ (𝐶 +R -1R) <R 𝐶) → 𝑦 <R 𝐶)
11833, 117mp3an3 1441 . . . . . . . . . . . 12 ((𝑦R ∧ ¬ (𝐶 +R -1R) <R 𝑦) → 𝑦 <R 𝐶)
119 breq2 5061 . . . . . . . . . . . . . . 15 (𝑧 = 𝐶 → (𝑦 <R 𝑧𝑦 <R 𝐶))
120119rspcev 3620 . . . . . . . . . . . . . 14 ((𝐶𝐴𝑦 <R 𝐶) → ∃𝑧𝐴 𝑦 <R 𝑧)
121120ex 413 . . . . . . . . . . . . 13 (𝐶𝐴 → (𝑦 <R 𝐶 → ∃𝑧𝐴 𝑦 <R 𝑧))
122121a1dd 50 . . . . . . . . . . . 12 (𝐶𝐴 → (𝑦 <R 𝐶 → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
123118, 122syl5 34 . . . . . . . . . . 11 (𝐶𝐴 → ((𝑦R ∧ ¬ (𝐶 +R -1R) <R 𝑦) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
124123expcomd 417 . . . . . . . . . 10 (𝐶𝐴 → (¬ (𝐶 +R -1R) <R 𝑦 → (𝑦R → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))))
125124ad2antrr 722 . . . . . . . . 9 (((𝐶𝐴𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → (¬ (𝐶 +R -1R) <R 𝑦 → (𝑦R → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))))
126116, 125pm2.61d 180 . . . . . . . 8 (((𝐶𝐴𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → (𝑦R → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
127126ralrimiv 3178 . . . . . . 7 (((𝐶𝐴𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))
128127ex 413 . . . . . 6 ((𝐶𝐴𝑣P) → (∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) → ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
129128adantlr 711 . . . . 5 (((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) ∧ 𝑣P) → (∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) → ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
13089, 129anim12d 608 . . . 4 (((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) ∧ 𝑣P) → ((∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → (∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))))
131 breq1 5060 . . . . . . . 8 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑥 <R 𝑦 ↔ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
132131notbid 319 . . . . . . 7 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (¬ 𝑥 <R 𝑦 ↔ ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
133132ralbidv 3194 . . . . . 6 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ↔ ∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
134 breq2 5061 . . . . . . . 8 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑦 <R 𝑥𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )))
135134imbi1d 343 . . . . . . 7 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧) ↔ (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
136135ralbidv 3194 . . . . . 6 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧) ↔ ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
137133, 136anbi12d 630 . . . . 5 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧)) ↔ (∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))))
138137rspcev 3620 . . . 4 (((𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R ∧ (∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧)))
13962, 130, 138syl6an 680 . . 3 (((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) ∧ 𝑣P) → ((∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧))))
140139rexlimdva 3281 . 2 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → (∃𝑣P (∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧))))
14157, 140mpd 15 1 ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wal 1526   = wceq 1528  wex 1771  wcel 2105  {cab 2796  wne 3013  wral 3135  wrex 3136  c0 4288  cop 4563   class class class wbr 5057  (class class class)co 7145  [cec 8276  Pcnp 10269  1Pc1p 10270  <P cltp 10273   ~R cer 10274  Rcnr 10275  0Rc0r 10276  1Rc1r 10277  -1Rcm1r 10278   +R cplr 10279   <R cltr 10281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-omul 8096  df-er 8278  df-ec 8280  df-qs 8284  df-ni 10282  df-pli 10283  df-mi 10284  df-lti 10285  df-plpq 10318  df-mpq 10319  df-ltpq 10320  df-enq 10321  df-nq 10322  df-erq 10323  df-plq 10324  df-mq 10325  df-1nq 10326  df-rq 10327  df-ltnq 10328  df-np 10391  df-1p 10392  df-plp 10393  df-mp 10394  df-ltp 10395  df-enr 10465  df-nr 10466  df-plr 10467  df-mr 10468  df-ltr 10469  df-0r 10470  df-1r 10471  df-m1r 10472
This theorem is referenced by:  supsr  10522
  Copyright terms: Public domain W3C validator