Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  suplocexprlemloc GIF version

Theorem suplocexprlemloc 7573
 Description: Lemma for suplocexpr 7577. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.)
Hypotheses
Ref Expression
suplocexpr.m (𝜑 → ∃𝑥 𝑥𝐴)
suplocexpr.ub (𝜑 → ∃𝑥P𝑦𝐴 𝑦<P 𝑥)
suplocexpr.loc (𝜑 → ∀𝑥P𝑦P (𝑥<P 𝑦 → (∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)))
suplocexpr.b 𝐵 = ⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩
Assertion
Ref Expression
suplocexprlemloc (𝜑 → ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞 (1st𝐴) ∨ 𝑟 ∈ (2nd𝐵))))
Distinct variable groups:   𝑢,𝐴,𝑧,𝑤   𝑥,𝐴,𝑦,𝑢,𝑧   𝑢,𝑞,𝑧,𝑤   𝑥,𝑞,𝑦,𝜑   𝜑,𝑟,𝑤,𝑞   𝜑,𝑧,𝑥,𝑦   𝑢,𝑟
Allowed substitution hints:   𝜑(𝑢)   𝐴(𝑟,𝑞)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑢,𝑟,𝑞)

Proof of Theorem suplocexprlemloc
Dummy variables 𝑠 𝑡 𝑣 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 109 . . . . 5 (((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) → 𝑞 <Q 𝑟)
2 ltbtwnnqq 7267 . . . . 5 (𝑞 <Q 𝑟 ↔ ∃𝑣Q (𝑞 <Q 𝑣𝑣 <Q 𝑟))
31, 2sylib 121 . . . 4 (((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) → ∃𝑣Q (𝑞 <Q 𝑣𝑣 <Q 𝑟))
4 simplll 523 . . . . . . 7 ((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) → 𝜑)
5 simprl 521 . . . . . . . 8 ((𝜑 ∧ (𝑞Q𝑟Q)) → 𝑞Q)
65ad2antrr 480 . . . . . . 7 ((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) → 𝑞Q)
7 simprl 521 . . . . . . 7 ((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) → 𝑣Q)
84, 6, 7jca32 308 . . . . . 6 ((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) → (𝜑 ∧ (𝑞Q𝑣Q)))
9 simprrl 529 . . . . . 6 ((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) → 𝑞 <Q 𝑣)
10 ltnqpri 7446 . . . . . . . . 9 (𝑞 <Q 𝑣 → ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩)
1110adantl 275 . . . . . . . 8 (((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) → ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩)
12 breq2 3942 . . . . . . . . . 10 (𝑦 = ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩ → (⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑦 ↔ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩))
13 breq2 3942 . . . . . . . . . . . 12 (𝑦 = ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩ → (𝑧<P 𝑦𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩))
1413ralbidv 2439 . . . . . . . . . . 11 (𝑦 = ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩ → (∀𝑧𝐴 𝑧<P 𝑦 ↔ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩))
1514orbi2d 780 . . . . . . . . . 10 (𝑦 = ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩ → ((∃𝑧𝐴 ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦) ↔ (∃𝑧𝐴 ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩)))
1612, 15imbi12d 233 . . . . . . . . 9 (𝑦 = ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩ → ((⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑦 → (∃𝑧𝐴 ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)) ↔ (⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩ → (∃𝑧𝐴 ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩))))
17 breq1 3941 . . . . . . . . . . . 12 (𝑥 = ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩ → (𝑥<P 𝑦 ↔ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑦))
18 breq1 3941 . . . . . . . . . . . . . 14 (𝑥 = ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩ → (𝑥<P 𝑧 ↔ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧))
1918rexbidv 2440 . . . . . . . . . . . . 13 (𝑥 = ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩ → (∃𝑧𝐴 𝑥<P 𝑧 ↔ ∃𝑧𝐴 ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧))
2019orbi1d 781 . . . . . . . . . . . 12 (𝑥 = ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩ → ((∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦) ↔ (∃𝑧𝐴 ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)))
2117, 20imbi12d 233 . . . . . . . . . . 11 (𝑥 = ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩ → ((𝑥<P 𝑦 → (∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)) ↔ (⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑦 → (∃𝑧𝐴 ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦))))
2221ralbidv 2439 . . . . . . . . . 10 (𝑥 = ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩ → (∀𝑦P (𝑥<P 𝑦 → (∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)) ↔ ∀𝑦P (⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑦 → (∃𝑧𝐴 ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦))))
23 suplocexpr.loc . . . . . . . . . . 11 (𝜑 → ∀𝑥P𝑦P (𝑥<P 𝑦 → (∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)))
2423ad2antrr 480 . . . . . . . . . 10 (((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) → ∀𝑥P𝑦P (𝑥<P 𝑦 → (∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)))
25 simplrl 525 . . . . . . . . . . 11 (((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) → 𝑞Q)
26 nqprlu 7399 . . . . . . . . . . 11 (𝑞Q → ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩ ∈ P)
2725, 26syl 14 . . . . . . . . . 10 (((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) → ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩ ∈ P)
2822, 24, 27rspcdva 2799 . . . . . . . . 9 (((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) → ∀𝑦P (⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑦 → (∃𝑧𝐴 ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)))
29 simplrr 526 . . . . . . . . . 10 (((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) → 𝑣Q)
30 nqprlu 7399 . . . . . . . . . 10 (𝑣Q → ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩ ∈ P)
3129, 30syl 14 . . . . . . . . 9 (((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) → ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩ ∈ P)
3216, 28, 31rspcdva 2799 . . . . . . . 8 (((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) → (⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩ → (∃𝑧𝐴 ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩)))
3311, 32mpd 13 . . . . . . 7 (((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) → (∃𝑧𝐴 ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩))
34 simpr 109 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) → ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧)
3527ad2antrr 480 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) → ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩ ∈ P)
36 suplocexpr.m . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑥 𝑥𝐴)
37 suplocexpr.ub . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑥P𝑦𝐴 𝑦<P 𝑥)
3836, 37, 23suplocexprlemss 7567 . . . . . . . . . . . . . . 15 (𝜑𝐴P)
3938ad4antr 486 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) → 𝐴P)
40 simplr 520 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) → 𝑧𝐴)
4139, 40sseldd 3104 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) → 𝑧P)
42 ltdfpr 7358 . . . . . . . . . . . . 13 ((⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩ ∈ P𝑧P) → (⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧 ↔ ∃𝑤Q (𝑤 ∈ (2nd ‘⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩) ∧ 𝑤 ∈ (1st𝑧))))
4335, 41, 42syl2anc 409 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) → (⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧 ↔ ∃𝑤Q (𝑤 ∈ (2nd ‘⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩) ∧ 𝑤 ∈ (1st𝑧))))
4434, 43mpbid 146 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) → ∃𝑤Q (𝑤 ∈ (2nd ‘⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩) ∧ 𝑤 ∈ (1st𝑧)))
45 vex 2693 . . . . . . . . . . . . . 14 𝑤 ∈ V
46 breq2 3942 . . . . . . . . . . . . . 14 (𝑢 = 𝑤 → (𝑞 <Q 𝑢𝑞 <Q 𝑤))
47 ltnqex 7401 . . . . . . . . . . . . . . 15 {𝑙𝑙 <Q 𝑞} ∈ V
48 gtnqex 7402 . . . . . . . . . . . . . . 15 {𝑢𝑞 <Q 𝑢} ∈ V
4947, 48op2nd 6054 . . . . . . . . . . . . . 14 (2nd ‘⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩) = {𝑢𝑞 <Q 𝑢}
5045, 46, 49elab2 2837 . . . . . . . . . . . . 13 (𝑤 ∈ (2nd ‘⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩) ↔ 𝑞 <Q 𝑤)
5150anbi1i 454 . . . . . . . . . . . 12 ((𝑤 ∈ (2nd ‘⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩) ∧ 𝑤 ∈ (1st𝑧)) ↔ (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))
5251rexbii 2446 . . . . . . . . . . 11 (∃𝑤Q (𝑤 ∈ (2nd ‘⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩) ∧ 𝑤 ∈ (1st𝑧)) ↔ ∃𝑤Q (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))
5344, 52sylib 121 . . . . . . . . . 10 (((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) → ∃𝑤Q (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))
54 simpllr 524 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) ∧ (𝑤Q ∧ (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))) → 𝑧𝐴)
55 simprrl 529 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) ∧ (𝑤Q ∧ (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))) → 𝑞 <Q 𝑤)
5641adantr 274 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) ∧ (𝑤Q ∧ (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))) → 𝑧P)
57 prop 7327 . . . . . . . . . . . . . . . . 17 (𝑧P → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ P)
5856, 57syl 14 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) ∧ (𝑤Q ∧ (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))) → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ P)
59 simprrr 530 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) ∧ (𝑤Q ∧ (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))) → 𝑤 ∈ (1st𝑧))
60 prcdnql 7336 . . . . . . . . . . . . . . . 16 ((⟨(1st𝑧), (2nd𝑧)⟩ ∈ P𝑤 ∈ (1st𝑧)) → (𝑞 <Q 𝑤𝑞 ∈ (1st𝑧)))
6158, 59, 60syl2anc 409 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) ∧ (𝑤Q ∧ (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))) → (𝑞 <Q 𝑤𝑞 ∈ (1st𝑧)))
6255, 61mpd 13 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) ∧ (𝑤Q ∧ (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))) → 𝑞 ∈ (1st𝑧))
6354, 62jca 304 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) ∧ (𝑤Q ∧ (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))) → (𝑧𝐴𝑞 ∈ (1st𝑧)))
646319.8ad 1571 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) ∧ (𝑤Q ∧ (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))) → ∃𝑧(𝑧𝐴𝑞 ∈ (1st𝑧)))
65 df-rex 2423 . . . . . . . . . . . 12 (∃𝑧𝐴 𝑞 ∈ (1st𝑧) ↔ ∃𝑧(𝑧𝐴𝑞 ∈ (1st𝑧)))
6664, 65sylibr 133 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) ∧ (𝑤Q ∧ (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))) → ∃𝑧𝐴 𝑞 ∈ (1st𝑧))
67 suplocexprlemell 7565 . . . . . . . . . . 11 (𝑞 (1st𝐴) ↔ ∃𝑧𝐴 𝑞 ∈ (1st𝑧))
6866, 67sylibr 133 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) ∧ (𝑤Q ∧ (𝑞 <Q 𝑤𝑤 ∈ (1st𝑧)))) → 𝑞 (1st𝐴))
6953, 68rexlimddv 2558 . . . . . . . . 9 (((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ 𝑧𝐴) ∧ ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧) → 𝑞 (1st𝐴))
7069rexlimdva2 2556 . . . . . . . 8 (((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) → (∃𝑧𝐴 ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧𝑞 (1st𝐴)))
71 fo2nd 6065 . . . . . . . . . . . . . . 15 2nd :V–onto→V
72 fofun 5355 . . . . . . . . . . . . . . 15 (2nd :V–onto→V → Fun 2nd )
7371, 72ax-mp 5 . . . . . . . . . . . . . 14 Fun 2nd
74 fvelima 5482 . . . . . . . . . . . . . 14 ((Fun 2nd𝑠 ∈ (2nd𝐴)) → ∃𝑡𝐴 (2nd𝑡) = 𝑠)
7573, 74mpan 421 . . . . . . . . . . . . 13 (𝑠 ∈ (2nd𝐴) → ∃𝑡𝐴 (2nd𝑡) = 𝑠)
7675adantl 275 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) ∧ 𝑠 ∈ (2nd𝐴)) → ∃𝑡𝐴 (2nd𝑡) = 𝑠)
77 breq1 3941 . . . . . . . . . . . . . . 15 (𝑧 = 𝑡 → (𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩ ↔ 𝑡<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩))
78 simpllr 524 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) ∧ 𝑠 ∈ (2nd𝐴)) ∧ (𝑡𝐴 ∧ (2nd𝑡) = 𝑠)) → ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩)
79 simprl 521 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) ∧ 𝑠 ∈ (2nd𝐴)) ∧ (𝑡𝐴 ∧ (2nd𝑡) = 𝑠)) → 𝑡𝐴)
8077, 78, 79rspcdva 2799 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) ∧ 𝑠 ∈ (2nd𝐴)) ∧ (𝑡𝐴 ∧ (2nd𝑡) = 𝑠)) → 𝑡<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩)
8129ad3antrrr 484 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) ∧ 𝑠 ∈ (2nd𝐴)) ∧ (𝑡𝐴 ∧ (2nd𝑡) = 𝑠)) → 𝑣Q)
8238ad5antr 488 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) ∧ 𝑠 ∈ (2nd𝐴)) ∧ (𝑡𝐴 ∧ (2nd𝑡) = 𝑠)) → 𝐴P)
8382, 79sseldd 3104 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) ∧ 𝑠 ∈ (2nd𝐴)) ∧ (𝑡𝐴 ∧ (2nd𝑡) = 𝑠)) → 𝑡P)
84 nqpru 7404 . . . . . . . . . . . . . . 15 ((𝑣Q𝑡P) → (𝑣 ∈ (2nd𝑡) ↔ 𝑡<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩))
8581, 83, 84syl2anc 409 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) ∧ 𝑠 ∈ (2nd𝐴)) ∧ (𝑡𝐴 ∧ (2nd𝑡) = 𝑠)) → (𝑣 ∈ (2nd𝑡) ↔ 𝑡<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩))
8680, 85mpbird 166 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) ∧ 𝑠 ∈ (2nd𝐴)) ∧ (𝑡𝐴 ∧ (2nd𝑡) = 𝑠)) → 𝑣 ∈ (2nd𝑡))
87 simprr 522 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) ∧ 𝑠 ∈ (2nd𝐴)) ∧ (𝑡𝐴 ∧ (2nd𝑡) = 𝑠)) → (2nd𝑡) = 𝑠)
8886, 87eleqtrd 2219 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) ∧ 𝑠 ∈ (2nd𝐴)) ∧ (𝑡𝐴 ∧ (2nd𝑡) = 𝑠)) → 𝑣𝑠)
8976, 88rexlimddv 2558 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) ∧ 𝑠 ∈ (2nd𝐴)) → 𝑣𝑠)
9089ralrimiva 2509 . . . . . . . . . 10 ((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) → ∀𝑠 ∈ (2nd𝐴)𝑣𝑠)
91 vex 2693 . . . . . . . . . . 11 𝑣 ∈ V
9291elint2 3787 . . . . . . . . . 10 (𝑣 (2nd𝐴) ↔ ∀𝑠 ∈ (2nd𝐴)𝑣𝑠)
9390, 92sylibr 133 . . . . . . . . 9 ((((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) ∧ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) → 𝑣 (2nd𝐴))
9493ex 114 . . . . . . . 8 (((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) → (∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩ → 𝑣 (2nd𝐴)))
9570, 94orim12d 776 . . . . . . 7 (((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) → ((∃𝑧𝐴 ⟨{𝑙𝑙 <Q 𝑞}, {𝑢𝑞 <Q 𝑢}⟩<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P ⟨{𝑙𝑙 <Q 𝑣}, {𝑢𝑣 <Q 𝑢}⟩) → (𝑞 (1st𝐴) ∨ 𝑣 (2nd𝐴))))
9633, 95mpd 13 . . . . . 6 (((𝜑 ∧ (𝑞Q𝑣Q)) ∧ 𝑞 <Q 𝑣) → (𝑞 (1st𝐴) ∨ 𝑣 (2nd𝐴)))
978, 9, 96syl2anc 409 . . . . 5 ((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) → (𝑞 (1st𝐴) ∨ 𝑣 (2nd𝐴)))
98 breq2 3942 . . . . . . . . . 10 (𝑢 = 𝑟 → (𝑤 <Q 𝑢𝑤 <Q 𝑟))
9998rexbidv 2440 . . . . . . . . 9 (𝑢 = 𝑟 → (∃𝑤 (2nd𝐴)𝑤 <Q 𝑢 ↔ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑟))
100 simprr 522 . . . . . . . . . 10 ((𝜑 ∧ (𝑞Q𝑟Q)) → 𝑟Q)
101100ad3antrrr 484 . . . . . . . . 9 (((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) ∧ 𝑣 (2nd𝐴)) → 𝑟Q)
102 simpr 109 . . . . . . . . . 10 (((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) ∧ 𝑣 (2nd𝐴)) → 𝑣 (2nd𝐴))
103 simprrr 530 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) → 𝑣 <Q 𝑟)
104103adantr 274 . . . . . . . . . 10 (((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) ∧ 𝑣 (2nd𝐴)) → 𝑣 <Q 𝑟)
105 breq1 3941 . . . . . . . . . . 11 (𝑤 = 𝑣 → (𝑤 <Q 𝑟𝑣 <Q 𝑟))
106105rspcev 2794 . . . . . . . . . 10 ((𝑣 (2nd𝐴) ∧ 𝑣 <Q 𝑟) → ∃𝑤 (2nd𝐴)𝑤 <Q 𝑟)
107102, 104, 106syl2anc 409 . . . . . . . . 9 (((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) ∧ 𝑣 (2nd𝐴)) → ∃𝑤 (2nd𝐴)𝑤 <Q 𝑟)
10899, 101, 107elrabd 2847 . . . . . . . 8 (((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) ∧ 𝑣 (2nd𝐴)) → 𝑟 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
109 suplocexpr.b . . . . . . . . . . . 12 𝐵 = ⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩
110109suplocexprlem2b 7566 . . . . . . . . . . 11 (𝐴P → (2nd𝐵) = {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
11138, 110syl 14 . . . . . . . . . 10 (𝜑 → (2nd𝐵) = {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
112111eleq2d 2210 . . . . . . . . 9 (𝜑 → (𝑟 ∈ (2nd𝐵) ↔ 𝑟 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}))
113112ad4antr 486 . . . . . . . 8 (((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) ∧ 𝑣 (2nd𝐴)) → (𝑟 ∈ (2nd𝐵) ↔ 𝑟 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}))
114108, 113mpbird 166 . . . . . . 7 (((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) ∧ 𝑣 (2nd𝐴)) → 𝑟 ∈ (2nd𝐵))
115114ex 114 . . . . . 6 ((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) → (𝑣 (2nd𝐴) → 𝑟 ∈ (2nd𝐵)))
116115orim2d 778 . . . . 5 ((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) → ((𝑞 (1st𝐴) ∨ 𝑣 (2nd𝐴)) → (𝑞 (1st𝐴) ∨ 𝑟 ∈ (2nd𝐵))))
11797, 116mpd 13 . . . 4 ((((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ (𝑣Q ∧ (𝑞 <Q 𝑣𝑣 <Q 𝑟))) → (𝑞 (1st𝐴) ∨ 𝑟 ∈ (2nd𝐵)))
1183, 117rexlimddv 2558 . . 3 (((𝜑 ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) → (𝑞 (1st𝐴) ∨ 𝑟 ∈ (2nd𝐵)))
119118ex 114 . 2 ((𝜑 ∧ (𝑞Q𝑟Q)) → (𝑞 <Q 𝑟 → (𝑞 (1st𝐴) ∨ 𝑟 ∈ (2nd𝐵))))
120119ralrimivva 2518 1 (𝜑 → ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞 (1st𝐴) ∨ 𝑟 ∈ (2nd𝐵))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   = wceq 1332  ∃wex 1469   ∈ wcel 1481  {cab 2126  ∀wral 2417  ∃wrex 2418  {crab 2421  Vcvv 2690   ⊆ wss 3077  ⟨cop 3536  ∪ cuni 3745  ∩ cint 3780   class class class wbr 3938   “ cima 4551  Fun wfun 5126  –onto→wfo 5130  ‘cfv 5132  1st c1st 6045  2nd c2nd 6046  Qcnq 7132
 Copyright terms: Public domain W3C validator