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

Theorem suplocexprlemlub 7525
 Description: Lemma for suplocexpr 7526. The putative supremum is a least 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
suplocexprlemlub (𝜑 → (𝑦<P 𝐵 → ∃𝑧𝐴 𝑦<P 𝑧))
Distinct variable groups:   𝑦,𝐴,𝑧   𝑥,𝐴,𝑦   𝑧,𝐵   𝜑,𝑦,𝑧   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑤,𝑢)   𝐴(𝑤,𝑢)   𝐵(𝑥,𝑦,𝑤,𝑢)

Proof of Theorem suplocexprlemlub
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 simpr 109 . . . 4 ((𝜑𝑦<P 𝐵) → 𝑦<P 𝐵)
2 ltrelpr 7306 . . . . . . . 8 <P ⊆ (P × P)
32brel 4586 . . . . . . 7 (𝑦<P 𝐵 → (𝑦P𝐵P))
43simpld 111 . . . . . 6 (𝑦<P 𝐵𝑦P)
54adantl 275 . . . . 5 ((𝜑𝑦<P 𝐵) → 𝑦P)
63simprd 113 . . . . . 6 (𝑦<P 𝐵𝐵P)
76adantl 275 . . . . 5 ((𝜑𝑦<P 𝐵) → 𝐵P)
8 ltdfpr 7307 . . . . 5 ((𝑦P𝐵P) → (𝑦<P 𝐵 ↔ ∃𝑠Q (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵))))
95, 7, 8syl2anc 408 . . . 4 ((𝜑𝑦<P 𝐵) → (𝑦<P 𝐵 ↔ ∃𝑠Q (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵))))
101, 9mpbid 146 . . 3 ((𝜑𝑦<P 𝐵) → ∃𝑠Q (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))
11 simprrr 529 . . . . . 6 (((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) → 𝑠 ∈ (1st𝐵))
12 suplocexpr.b . . . . . . . . . 10 𝐵 = ⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩
1312fveq2i 5417 . . . . . . . . 9 (1st𝐵) = (1st ‘⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩)
14 npex 7274 . . . . . . . . . . . . 13 P ∈ V
1514a1i 9 . . . . . . . . . . . 12 (𝜑P ∈ V)
16 suplocexpr.m . . . . . . . . . . . . 13 (𝜑 → ∃𝑥 𝑥𝐴)
17 suplocexpr.ub . . . . . . . . . . . . 13 (𝜑 → ∃𝑥P𝑦𝐴 𝑦<P 𝑥)
18 suplocexpr.loc . . . . . . . . . . . . 13 (𝜑 → ∀𝑥P𝑦P (𝑥<P 𝑦 → (∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)))
1916, 17, 18suplocexprlemss 7516 . . . . . . . . . . . 12 (𝜑𝐴P)
2015, 19ssexd 4063 . . . . . . . . . . 11 (𝜑𝐴 ∈ V)
21 fo1st 6048 . . . . . . . . . . . . 13 1st :V–onto→V
22 fofun 5341 . . . . . . . . . . . . 13 (1st :V–onto→V → Fun 1st )
2321, 22ax-mp 5 . . . . . . . . . . . 12 Fun 1st
24 funimaexg 5202 . . . . . . . . . . . 12 ((Fun 1st𝐴 ∈ V) → (1st𝐴) ∈ V)
2523, 24mpan 420 . . . . . . . . . . 11 (𝐴 ∈ V → (1st𝐴) ∈ V)
26 uniexg 4356 . . . . . . . . . . 11 ((1st𝐴) ∈ V → (1st𝐴) ∈ V)
2720, 25, 263syl 17 . . . . . . . . . 10 (𝜑 (1st𝐴) ∈ V)
28 nqex 7164 . . . . . . . . . . 11 Q ∈ V
2928rabex 4067 . . . . . . . . . 10 {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢} ∈ V
30 op1stg 6041 . . . . . . . . . 10 (( (1st𝐴) ∈ V ∧ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢} ∈ V) → (1st ‘⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩) = (1st𝐴))
3127, 29, 30sylancl 409 . . . . . . . . 9 (𝜑 → (1st ‘⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩) = (1st𝐴))
3213, 31syl5eq 2182 . . . . . . . 8 (𝜑 → (1st𝐵) = (1st𝐴))
3332eleq2d 2207 . . . . . . 7 (𝜑 → (𝑠 ∈ (1st𝐵) ↔ 𝑠 (1st𝐴)))
3433ad2antrr 479 . . . . . 6 (((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) → (𝑠 ∈ (1st𝐵) ↔ 𝑠 (1st𝐴)))
3511, 34mpbid 146 . . . . 5 (((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) → 𝑠 (1st𝐴))
36 suplocexprlemell 7514 . . . . 5 (𝑠 (1st𝐴) ↔ ∃𝑧𝐴 𝑠 ∈ (1st𝑧))
3735, 36sylib 121 . . . 4 (((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) → ∃𝑧𝐴 𝑠 ∈ (1st𝑧))
38 simprl 520 . . . . . . . . 9 (((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) → 𝑠Q)
3938ad2antrr 479 . . . . . . . 8 (((((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) ∧ 𝑧𝐴) ∧ 𝑠 ∈ (1st𝑧)) → 𝑠Q)
40 simprrl 528 . . . . . . . . 9 (((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) → 𝑠 ∈ (2nd𝑦))
4140ad2antrr 479 . . . . . . . 8 (((((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) ∧ 𝑧𝐴) ∧ 𝑠 ∈ (1st𝑧)) → 𝑠 ∈ (2nd𝑦))
42 simpr 109 . . . . . . . 8 (((((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) ∧ 𝑧𝐴) ∧ 𝑠 ∈ (1st𝑧)) → 𝑠 ∈ (1st𝑧))
43 rspe 2479 . . . . . . . 8 ((𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝑧))) → ∃𝑠Q (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝑧)))
4439, 41, 42, 43syl12anc 1214 . . . . . . 7 (((((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) ∧ 𝑧𝐴) ∧ 𝑠 ∈ (1st𝑧)) → ∃𝑠Q (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝑧)))
454ad4antlr 486 . . . . . . . 8 (((((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) ∧ 𝑧𝐴) ∧ 𝑠 ∈ (1st𝑧)) → 𝑦P)
4619ad4antr 485 . . . . . . . . 9 (((((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) ∧ 𝑧𝐴) ∧ 𝑠 ∈ (1st𝑧)) → 𝐴P)
47 simplr 519 . . . . . . . . 9 (((((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) ∧ 𝑧𝐴) ∧ 𝑠 ∈ (1st𝑧)) → 𝑧𝐴)
4846, 47sseldd 3093 . . . . . . . 8 (((((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) ∧ 𝑧𝐴) ∧ 𝑠 ∈ (1st𝑧)) → 𝑧P)
49 ltdfpr 7307 . . . . . . . 8 ((𝑦P𝑧P) → (𝑦<P 𝑧 ↔ ∃𝑠Q (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝑧))))
5045, 48, 49syl2anc 408 . . . . . . 7 (((((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) ∧ 𝑧𝐴) ∧ 𝑠 ∈ (1st𝑧)) → (𝑦<P 𝑧 ↔ ∃𝑠Q (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝑧))))
5144, 50mpbird 166 . . . . . 6 (((((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) ∧ 𝑧𝐴) ∧ 𝑠 ∈ (1st𝑧)) → 𝑦<P 𝑧)
5251ex 114 . . . . 5 ((((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) ∧ 𝑧𝐴) → (𝑠 ∈ (1st𝑧) → 𝑦<P 𝑧))
5352reximdva 2532 . . . 4 (((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) → (∃𝑧𝐴 𝑠 ∈ (1st𝑧) → ∃𝑧𝐴 𝑦<P 𝑧))
5437, 53mpd 13 . . 3 (((𝜑𝑦<P 𝐵) ∧ (𝑠Q ∧ (𝑠 ∈ (2nd𝑦) ∧ 𝑠 ∈ (1st𝐵)))) → ∃𝑧𝐴 𝑦<P 𝑧)
5510, 54rexlimddv 2552 . 2 ((𝜑𝑦<P 𝐵) → ∃𝑧𝐴 𝑦<P 𝑧)
5655ex 114 1 (𝜑 → (𝑦<P 𝐵 → ∃𝑧𝐴 𝑦<P 𝑧))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697   = wceq 1331  ∃wex 1468   ∈ wcel 1480  ∀wral 2414  ∃wrex 2415  {crab 2418  Vcvv 2681   ⊆ wss 3066  ⟨cop 3525  ∪ cuni 3731  ∩ cint 3766   class class class wbr 3924   “ cima 4537  Fun wfun 5112  –onto→wfo 5116  ‘cfv 5118  1st c1st 6029  2nd c2nd 6030  Qcnq 7081
 Copyright terms: Public domain W3C validator