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

Theorem suplocexprlemdisj 7540
 Description: Lemma for suplocexpr 7545. The putative supremum is disjoint. (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
suplocexprlemdisj (𝜑 → ∀𝑞Q ¬ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵)))
Distinct variable groups:   𝑤,𝐴,𝑢   𝑥,𝐴,𝑦   𝑤,𝐵   𝜑,𝑞,𝑤   𝜑,𝑥,𝑦   𝑢,𝑞
Allowed substitution hints:   𝜑(𝑧,𝑢)   𝐴(𝑧,𝑞)   𝐵(𝑥,𝑦,𝑧,𝑢,𝑞)

Proof of Theorem suplocexprlemdisj
Dummy variables 𝑠 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprl 520 . . . . 5 (((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) → 𝑞 (1st𝐴))
2 suplocexprlemell 7533 . . . . 5 (𝑞 (1st𝐴) ↔ ∃𝑠𝐴 𝑞 ∈ (1st𝑠))
31, 2sylib 121 . . . 4 (((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) → ∃𝑠𝐴 𝑞 ∈ (1st𝑠))
4 simprr 521 . . . . . 6 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → 𝑞 ∈ (1st𝑠))
5 simplrr 525 . . . . . . . . 9 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → 𝑞 ∈ (2nd𝐵))
6 suplocexpr.m . . . . . . . . . . . . 13 (𝜑 → ∃𝑥 𝑥𝐴)
7 suplocexpr.ub . . . . . . . . . . . . 13 (𝜑 → ∃𝑥P𝑦𝐴 𝑦<P 𝑥)
8 suplocexpr.loc . . . . . . . . . . . . 13 (𝜑 → ∀𝑥P𝑦P (𝑥<P 𝑦 → (∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)))
96, 7, 8suplocexprlemss 7535 . . . . . . . . . . . 12 (𝜑𝐴P)
109ad3antrrr 483 . . . . . . . . . . 11 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → 𝐴P)
11 suplocexpr.b . . . . . . . . . . . . 13 𝐵 = ⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩
1211suplocexprlem2b 7534 . . . . . . . . . . . 12 (𝐴P → (2nd𝐵) = {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
1312eleq2d 2209 . . . . . . . . . . 11 (𝐴P → (𝑞 ∈ (2nd𝐵) ↔ 𝑞 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}))
1410, 13syl 14 . . . . . . . . . 10 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → (𝑞 ∈ (2nd𝐵) ↔ 𝑞 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}))
15 breq2 3933 . . . . . . . . . . . 12 (𝑢 = 𝑞 → (𝑤 <Q 𝑢𝑤 <Q 𝑞))
1615rexbidv 2438 . . . . . . . . . . 11 (𝑢 = 𝑞 → (∃𝑤 (2nd𝐴)𝑤 <Q 𝑢 ↔ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑞))
1716elrab 2840 . . . . . . . . . 10 (𝑞 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢} ↔ (𝑞Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑞))
1814, 17syl6bb 195 . . . . . . . . 9 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → (𝑞 ∈ (2nd𝐵) ↔ (𝑞Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑞)))
195, 18mpbid 146 . . . . . . . 8 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → (𝑞Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑞))
2019simprd 113 . . . . . . 7 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → ∃𝑤 (2nd𝐴)𝑤 <Q 𝑞)
21 simprr 521 . . . . . . . 8 (((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑞)) → 𝑤 <Q 𝑞)
2210adantr 274 . . . . . . . . . . 11 (((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑞)) → 𝐴P)
23 simplrl 524 . . . . . . . . . . 11 (((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑞)) → 𝑠𝐴)
2422, 23sseldd 3098 . . . . . . . . . 10 (((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑞)) → 𝑠P)
25 prop 7295 . . . . . . . . . 10 (𝑠P → ⟨(1st𝑠), (2nd𝑠)⟩ ∈ P)
2624, 25syl 14 . . . . . . . . 9 (((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑞)) → ⟨(1st𝑠), (2nd𝑠)⟩ ∈ P)
27 eleq2 2203 . . . . . . . . . 10 (𝑡 = (2nd𝑠) → (𝑤𝑡𝑤 ∈ (2nd𝑠)))
28 simprl 520 . . . . . . . . . . 11 (((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑞)) → 𝑤 (2nd𝐴))
29 vex 2689 . . . . . . . . . . . 12 𝑤 ∈ V
3029elint2 3778 . . . . . . . . . . 11 (𝑤 (2nd𝐴) ↔ ∀𝑡 ∈ (2nd𝐴)𝑤𝑡)
3128, 30sylib 121 . . . . . . . . . 10 (((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑞)) → ∀𝑡 ∈ (2nd𝐴)𝑤𝑡)
32 fo2nd 6056 . . . . . . . . . . . . . 14 2nd :V–onto→V
33 fofun 5346 . . . . . . . . . . . . . 14 (2nd :V–onto→V → Fun 2nd )
3432, 33ax-mp 5 . . . . . . . . . . . . 13 Fun 2nd
35 vex 2689 . . . . . . . . . . . . . 14 𝑠 ∈ V
36 fof 5345 . . . . . . . . . . . . . . . 16 (2nd :V–onto→V → 2nd :V⟶V)
3732, 36ax-mp 5 . . . . . . . . . . . . . . 15 2nd :V⟶V
3837fdmi 5280 . . . . . . . . . . . . . 14 dom 2nd = V
3935, 38eleqtrri 2215 . . . . . . . . . . . . 13 𝑠 ∈ dom 2nd
40 funfvima 5649 . . . . . . . . . . . . 13 ((Fun 2nd𝑠 ∈ dom 2nd ) → (𝑠𝐴 → (2nd𝑠) ∈ (2nd𝐴)))
4134, 39, 40mp2an 422 . . . . . . . . . . . 12 (𝑠𝐴 → (2nd𝑠) ∈ (2nd𝐴))
4241ad2antrl 481 . . . . . . . . . . 11 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → (2nd𝑠) ∈ (2nd𝐴))
4342adantr 274 . . . . . . . . . 10 (((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑞)) → (2nd𝑠) ∈ (2nd𝐴))
4427, 31, 43rspcdva 2794 . . . . . . . . 9 (((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑞)) → 𝑤 ∈ (2nd𝑠))
45 prcunqu 7305 . . . . . . . . 9 ((⟨(1st𝑠), (2nd𝑠)⟩ ∈ P𝑤 ∈ (2nd𝑠)) → (𝑤 <Q 𝑞𝑞 ∈ (2nd𝑠)))
4626, 44, 45syl2anc 408 . . . . . . . 8 (((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑞)) → (𝑤 <Q 𝑞𝑞 ∈ (2nd𝑠)))
4721, 46mpd 13 . . . . . . 7 (((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑞)) → 𝑞 ∈ (2nd𝑠))
4820, 47rexlimddv 2554 . . . . . 6 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → 𝑞 ∈ (2nd𝑠))
494, 48jca 304 . . . . 5 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → (𝑞 ∈ (1st𝑠) ∧ 𝑞 ∈ (2nd𝑠)))
50 simprl 520 . . . . . . . 8 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → 𝑠𝐴)
5110, 50sseldd 3098 . . . . . . 7 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → 𝑠P)
5251, 25syl 14 . . . . . 6 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → ⟨(1st𝑠), (2nd𝑠)⟩ ∈ P)
53 simpllr 523 . . . . . 6 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → 𝑞Q)
54 prdisj 7312 . . . . . 6 ((⟨(1st𝑠), (2nd𝑠)⟩ ∈ P𝑞Q) → ¬ (𝑞 ∈ (1st𝑠) ∧ 𝑞 ∈ (2nd𝑠)))
5552, 53, 54syl2anc 408 . . . . 5 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → ¬ (𝑞 ∈ (1st𝑠) ∧ 𝑞 ∈ (2nd𝑠)))
5649, 55pm2.21fal 1351 . . . 4 ((((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) ∧ (𝑠𝐴𝑞 ∈ (1st𝑠))) → ⊥)
573, 56rexlimddv 2554 . . 3 (((𝜑𝑞Q) ∧ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵))) → ⊥)
5857inegd 1350 . 2 ((𝜑𝑞Q) → ¬ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵)))
5958ralrimiva 2505 1 (𝜑 → ∀𝑞Q ¬ (𝑞 (1st𝐴) ∧ 𝑞 ∈ (2nd𝐵)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697   = wceq 1331  ⊥wfal 1336  ∃wex 1468   ∈ wcel 1480  ∀wral 2416  ∃wrex 2417  {crab 2420  Vcvv 2686   ⊆ wss 3071  ⟨cop 3530  ∪ cuni 3736  ∩ cint 3771   class class class wbr 3929  dom cdm 4539   “ cima 4542  Fun wfun 5117  ⟶wf 5119  –onto→wfo 5121  ‘cfv 5123  1st c1st 6036  2nd c2nd 6037  Qcnq 7100
 Copyright terms: Public domain W3C validator