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

Theorem suplocexprlemub 7543
 Description: Lemma for suplocexpr 7545. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-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
suplocexprlemub (𝜑 → ∀𝑦𝐴 ¬ 𝐵<P 𝑦)
Distinct variable groups:   𝑢,𝐴,𝑤,𝑦   𝑥,𝐴,𝑧,𝑢,𝑦   𝑤,𝐵   𝜑,𝑢,𝑤,𝑦   𝜑,𝑥,𝑧   𝑧,𝑤
Allowed substitution hints:   𝐵(𝑥,𝑦,𝑧,𝑢)

Proof of Theorem suplocexprlemub
Dummy variables 𝑠 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 109 . . . . 5 (((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) → 𝐵<P 𝑦)
2 suplocexpr.m . . . . . . . 8 (𝜑 → ∃𝑥 𝑥𝐴)
3 suplocexpr.ub . . . . . . . 8 (𝜑 → ∃𝑥P𝑦𝐴 𝑦<P 𝑥)
4 suplocexpr.loc . . . . . . . 8 (𝜑 → ∀𝑥P𝑦P (𝑥<P 𝑦 → (∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)))
5 suplocexpr.b . . . . . . . 8 𝐵 = ⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩
62, 3, 4, 5suplocexprlemex 7542 . . . . . . 7 (𝜑𝐵P)
76ad2antrr 479 . . . . . 6 (((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) → 𝐵P)
82, 3, 4suplocexprlemss 7535 . . . . . . . 8 (𝜑𝐴P)
98ad2antrr 479 . . . . . . 7 (((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) → 𝐴P)
10 simplr 519 . . . . . . 7 (((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) → 𝑦𝐴)
119, 10sseldd 3098 . . . . . 6 (((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) → 𝑦P)
12 ltdfpr 7326 . . . . . 6 ((𝐵P𝑦P) → (𝐵<P 𝑦 ↔ ∃𝑠Q (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦))))
137, 11, 12syl2anc 408 . . . . 5 (((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) → (𝐵<P 𝑦 ↔ ∃𝑠Q (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦))))
141, 13mpbid 146 . . . 4 (((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) → ∃𝑠Q (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))
15 simprrl 528 . . . . . . . 8 ((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) → 𝑠 ∈ (2nd𝐵))
165suplocexprlem2b 7534 . . . . . . . . . . 11 (𝐴P → (2nd𝐵) = {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
178, 16syl 14 . . . . . . . . . 10 (𝜑 → (2nd𝐵) = {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
1817eleq2d 2209 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (2nd𝐵) ↔ 𝑠 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}))
1918ad3antrrr 483 . . . . . . . 8 ((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) → (𝑠 ∈ (2nd𝐵) ↔ 𝑠 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}))
2015, 19mpbid 146 . . . . . . 7 ((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) → 𝑠 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
21 breq2 3933 . . . . . . . . 9 (𝑢 = 𝑠 → (𝑤 <Q 𝑢𝑤 <Q 𝑠))
2221rexbidv 2438 . . . . . . . 8 (𝑢 = 𝑠 → (∃𝑤 (2nd𝐴)𝑤 <Q 𝑢 ↔ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑠))
2322elrab 2840 . . . . . . 7 (𝑠 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢} ↔ (𝑠Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑠))
2420, 23sylib 121 . . . . . 6 ((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) → (𝑠Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑠))
2524simprd 113 . . . . 5 ((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) → ∃𝑤 (2nd𝐴)𝑤 <Q 𝑠)
26 simprrr 529 . . . . . . . 8 ((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) → 𝑠 ∈ (1st𝑦))
2726adantr 274 . . . . . . 7 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → 𝑠 ∈ (1st𝑦))
28 simprr 521 . . . . . . . 8 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → 𝑤 <Q 𝑠)
2911ad2antrr 479 . . . . . . . . . 10 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → 𝑦P)
30 prop 7295 . . . . . . . . . 10 (𝑦P → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ P)
3129, 30syl 14 . . . . . . . . 9 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ P)
32 eleq2 2203 . . . . . . . . . 10 (𝑡 = (2nd𝑦) → (𝑤𝑡𝑤 ∈ (2nd𝑦)))
33 simprl 520 . . . . . . . . . . 11 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → 𝑤 (2nd𝐴))
34 vex 2689 . . . . . . . . . . . 12 𝑤 ∈ V
3534elint2 3778 . . . . . . . . . . 11 (𝑤 (2nd𝐴) ↔ ∀𝑡 ∈ (2nd𝐴)𝑤𝑡)
3633, 35sylib 121 . . . . . . . . . 10 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → ∀𝑡 ∈ (2nd𝐴)𝑤𝑡)
37 fo2nd 6056 . . . . . . . . . . . . 13 2nd :V–onto→V
38 fofun 5346 . . . . . . . . . . . . 13 (2nd :V–onto→V → Fun 2nd )
3937, 38ax-mp 5 . . . . . . . . . . . 12 Fun 2nd
40 vex 2689 . . . . . . . . . . . . 13 𝑦 ∈ V
41 fof 5345 . . . . . . . . . . . . . . 15 (2nd :V–onto→V → 2nd :V⟶V)
4237, 41ax-mp 5 . . . . . . . . . . . . . 14 2nd :V⟶V
4342fdmi 5280 . . . . . . . . . . . . 13 dom 2nd = V
4440, 43eleqtrri 2215 . . . . . . . . . . . 12 𝑦 ∈ dom 2nd
45 funfvima 5649 . . . . . . . . . . . 12 ((Fun 2nd𝑦 ∈ dom 2nd ) → (𝑦𝐴 → (2nd𝑦) ∈ (2nd𝐴)))
4639, 44, 45mp2an 422 . . . . . . . . . . 11 (𝑦𝐴 → (2nd𝑦) ∈ (2nd𝐴))
4746ad4antlr 486 . . . . . . . . . 10 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → (2nd𝑦) ∈ (2nd𝐴))
4832, 36, 47rspcdva 2794 . . . . . . . . 9 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → 𝑤 ∈ (2nd𝑦))
49 prcunqu 7305 . . . . . . . . 9 ((⟨(1st𝑦), (2nd𝑦)⟩ ∈ P𝑤 ∈ (2nd𝑦)) → (𝑤 <Q 𝑠𝑠 ∈ (2nd𝑦)))
5031, 48, 49syl2anc 408 . . . . . . . 8 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → (𝑤 <Q 𝑠𝑠 ∈ (2nd𝑦)))
5128, 50mpd 13 . . . . . . 7 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → 𝑠 ∈ (2nd𝑦))
5227, 51jca 304 . . . . . 6 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → (𝑠 ∈ (1st𝑦) ∧ 𝑠 ∈ (2nd𝑦)))
53 simplrl 524 . . . . . . 7 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → 𝑠Q)
54 prdisj 7312 . . . . . . 7 ((⟨(1st𝑦), (2nd𝑦)⟩ ∈ P𝑠Q) → ¬ (𝑠 ∈ (1st𝑦) ∧ 𝑠 ∈ (2nd𝑦)))
5531, 53, 54syl2anc 408 . . . . . 6 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → ¬ (𝑠 ∈ (1st𝑦) ∧ 𝑠 ∈ (2nd𝑦)))
5652, 55pm2.21fal 1351 . . . . 5 (((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑠)) → ⊥)
5725, 56rexlimddv 2554 . . . 4 ((((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝐵) ∧ 𝑠 ∈ (1st𝑦)))) → ⊥)
5814, 57rexlimddv 2554 . . 3 (((𝜑𝑦𝐴) ∧ 𝐵<P 𝑦) → ⊥)
5958inegd 1350 . 2 ((𝜑𝑦𝐴) → ¬ 𝐵<P 𝑦)
6059ralrimiva 2505 1 (𝜑 → ∀𝑦𝐴 ¬ 𝐵<P 𝑦)
 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