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

Theorem suplocexprlemmu 7519
 Description: Lemma for suplocexpr 7526. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-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
suplocexprlemmu (𝜑 → ∃𝑠Q 𝑠 ∈ (2nd𝐵))
Distinct variable groups:   𝐴,𝑠,𝑢,𝑤   𝑥,𝐴,𝑦,𝑠,𝑢   𝐵,𝑠   𝜑,𝑠,𝑢,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑧,𝑤)   𝐴(𝑧)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑢)

Proof of Theorem suplocexprlemmu
Dummy variables 𝑗 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 suplocexpr.ub . . . 4 (𝜑 → ∃𝑥P𝑦𝐴 𝑦<P 𝑥)
2 prop 7276 . . . . . . 7 (𝑥P → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ P)
3 prmu 7279 . . . . . . 7 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ P → ∃𝑠Q 𝑠 ∈ (2nd𝑥))
42, 3syl 14 . . . . . 6 (𝑥P → ∃𝑠Q 𝑠 ∈ (2nd𝑥))
54ad2antrl 481 . . . . 5 ((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) → ∃𝑠Q 𝑠 ∈ (2nd𝑥))
6 fo2nd 6049 . . . . . . . . . . . . 13 2nd :V–onto→V
7 fofun 5341 . . . . . . . . . . . . 13 (2nd :V–onto→V → Fun 2nd )
86, 7ax-mp 5 . . . . . . . . . . . 12 Fun 2nd
9 fvelima 5466 . . . . . . . . . . . 12 ((Fun 2nd𝑡 ∈ (2nd𝐴)) → ∃𝑢𝐴 (2nd𝑢) = 𝑡)
108, 9mpan 420 . . . . . . . . . . 11 (𝑡 ∈ (2nd𝐴) → ∃𝑢𝐴 (2nd𝑢) = 𝑡)
1110adantl 275 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) → ∃𝑢𝐴 (2nd𝑢) = 𝑡)
12 suplocexpr.m . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑥 𝑥𝐴)
13 suplocexpr.loc . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑥P𝑦P (𝑥<P 𝑦 → (∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)))
1412, 1, 13suplocexprlemss 7516 . . . . . . . . . . . . . . 15 (𝜑𝐴P)
1514ad5antr 487 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → 𝐴P)
16 simprl 520 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → 𝑢𝐴)
1715, 16sseldd 3093 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → 𝑢P)
18 simprl 520 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) → 𝑥P)
1918ad4antr 485 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → 𝑥P)
20 breq1 3927 . . . . . . . . . . . . . . 15 (𝑦 = 𝑢 → (𝑦<P 𝑥𝑢<P 𝑥))
21 simprr 521 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) → ∀𝑦𝐴 𝑦<P 𝑥)
2221ad4antr 485 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → ∀𝑦𝐴 𝑦<P 𝑥)
2320, 22, 16rspcdva 2789 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → 𝑢<P 𝑥)
24 ltsopr 7397 . . . . . . . . . . . . . . . . 17 <P Or P
25 so2nr 4238 . . . . . . . . . . . . . . . . 17 ((<P Or P ∧ (𝑢P𝑥P)) → ¬ (𝑢<P 𝑥𝑥<P 𝑢))
2624, 25mpan 420 . . . . . . . . . . . . . . . 16 ((𝑢P𝑥P) → ¬ (𝑢<P 𝑥𝑥<P 𝑢))
2717, 19, 26syl2anc 408 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → ¬ (𝑢<P 𝑥𝑥<P 𝑢))
28 imnan 679 . . . . . . . . . . . . . . 15 ((𝑢<P 𝑥 → ¬ 𝑥<P 𝑢) ↔ ¬ (𝑢<P 𝑥𝑥<P 𝑢))
2927, 28sylibr 133 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → (𝑢<P 𝑥 → ¬ 𝑥<P 𝑢))
3023, 29mpd 13 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → ¬ 𝑥<P 𝑢)
31 aptiprlemu 7441 . . . . . . . . . . . . 13 ((𝑢P𝑥P ∧ ¬ 𝑥<P 𝑢) → (2nd𝑥) ⊆ (2nd𝑢))
3217, 19, 30, 31syl3anc 1216 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → (2nd𝑥) ⊆ (2nd𝑢))
33 simpllr 523 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → 𝑠 ∈ (2nd𝑥))
3432, 33sseldd 3093 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → 𝑠 ∈ (2nd𝑢))
35 simprr 521 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → (2nd𝑢) = 𝑡)
3634, 35eleqtrd 2216 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) ∧ (𝑢𝐴 ∧ (2nd𝑢) = 𝑡)) → 𝑠𝑡)
3711, 36rexlimddv 2552 . . . . . . . . 9 (((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) ∧ 𝑡 ∈ (2nd𝐴)) → 𝑠𝑡)
3837ralrimiva 2503 . . . . . . . 8 ((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) → ∀𝑡 ∈ (2nd𝐴)𝑠𝑡)
39 vex 2684 . . . . . . . . 9 𝑠 ∈ V
4039elint2 3773 . . . . . . . 8 (𝑠 (2nd𝐴) ↔ ∀𝑡 ∈ (2nd𝐴)𝑠𝑡)
4138, 40sylibr 133 . . . . . . 7 ((((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) ∧ 𝑠 ∈ (2nd𝑥)) → 𝑠 (2nd𝐴))
4241ex 114 . . . . . 6 (((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) ∧ 𝑠Q) → (𝑠 ∈ (2nd𝑥) → 𝑠 (2nd𝐴)))
4342reximdva 2532 . . . . 5 ((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) → (∃𝑠Q 𝑠 ∈ (2nd𝑥) → ∃𝑠Q 𝑠 (2nd𝐴)))
445, 43mpd 13 . . . 4 ((𝜑 ∧ (𝑥P ∧ ∀𝑦𝐴 𝑦<P 𝑥)) → ∃𝑠Q 𝑠 (2nd𝐴))
451, 44rexlimddv 2552 . . 3 (𝜑 → ∃𝑠Q 𝑠 (2nd𝐴))
46 simprr 521 . . . . . . 7 ((𝜑 ∧ (𝑠Q𝑠 (2nd𝐴))) → 𝑠 (2nd𝐴))
47 simprl 520 . . . . . . . . 9 ((𝜑 ∧ (𝑠Q𝑠 (2nd𝐴))) → 𝑠Q)
48 1nq 7167 . . . . . . . . 9 1QQ
49 addclnq 7176 . . . . . . . . 9 ((𝑠Q ∧ 1QQ) → (𝑠 +Q 1Q) ∈ Q)
5047, 48, 49sylancl 409 . . . . . . . 8 ((𝜑 ∧ (𝑠Q𝑠 (2nd𝐴))) → (𝑠 +Q 1Q) ∈ Q)
51 ltaddnq 7208 . . . . . . . . 9 ((𝑠Q ∧ 1QQ) → 𝑠 <Q (𝑠 +Q 1Q))
5247, 48, 51sylancl 409 . . . . . . . 8 ((𝜑 ∧ (𝑠Q𝑠 (2nd𝐴))) → 𝑠 <Q (𝑠 +Q 1Q))
53 breq2 3928 . . . . . . . . 9 (𝑗 = (𝑠 +Q 1Q) → (𝑠 <Q 𝑗𝑠 <Q (𝑠 +Q 1Q)))
5453rspcev 2784 . . . . . . . 8 (((𝑠 +Q 1Q) ∈ Q𝑠 <Q (𝑠 +Q 1Q)) → ∃𝑗Q 𝑠 <Q 𝑗)
5550, 52, 54syl2anc 408 . . . . . . 7 ((𝜑 ∧ (𝑠Q𝑠 (2nd𝐴))) → ∃𝑗Q 𝑠 <Q 𝑗)
56 breq1 3927 . . . . . . . . 9 (𝑤 = 𝑠 → (𝑤 <Q 𝑗𝑠 <Q 𝑗))
5756rexbidv 2436 . . . . . . . 8 (𝑤 = 𝑠 → (∃𝑗Q 𝑤 <Q 𝑗 ↔ ∃𝑗Q 𝑠 <Q 𝑗))
5857rspcev 2784 . . . . . . 7 ((𝑠 (2nd𝐴) ∧ ∃𝑗Q 𝑠 <Q 𝑗) → ∃𝑤 (2nd𝐴)∃𝑗Q 𝑤 <Q 𝑗)
5946, 55, 58syl2anc 408 . . . . . 6 ((𝜑 ∧ (𝑠Q𝑠 (2nd𝐴))) → ∃𝑤 (2nd𝐴)∃𝑗Q 𝑤 <Q 𝑗)
60 rexcom 2593 . . . . . 6 (∃𝑤 (2nd𝐴)∃𝑗Q 𝑤 <Q 𝑗 ↔ ∃𝑗Q𝑤 (2nd𝐴)𝑤 <Q 𝑗)
6159, 60sylib 121 . . . . 5 ((𝜑 ∧ (𝑠Q𝑠 (2nd𝐴))) → ∃𝑗Q𝑤 (2nd𝐴)𝑤 <Q 𝑗)
62 ssid 3112 . . . . . 6 QQ
63 rexss 3159 . . . . . 6 (QQ → (∃𝑗Q𝑤 (2nd𝐴)𝑤 <Q 𝑗 ↔ ∃𝑗Q (𝑗Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑗)))
6462, 63ax-mp 5 . . . . 5 (∃𝑗Q𝑤 (2nd𝐴)𝑤 <Q 𝑗 ↔ ∃𝑗Q (𝑗Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑗))
6561, 64sylib 121 . . . 4 ((𝜑 ∧ (𝑠Q𝑠 (2nd𝐴))) → ∃𝑗Q (𝑗Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑗))
66 suplocexpr.b . . . . . . . . . 10 𝐵 = ⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩
6766suplocexprlem2b 7515 . . . . . . . . 9 (𝐴P → (2nd𝐵) = {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
6814, 67syl 14 . . . . . . . 8 (𝜑 → (2nd𝐵) = {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
6968eleq2d 2207 . . . . . . 7 (𝜑 → (𝑗 ∈ (2nd𝐵) ↔ 𝑗 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}))
70 breq2 3928 . . . . . . . . 9 (𝑢 = 𝑗 → (𝑤 <Q 𝑢𝑤 <Q 𝑗))
7170rexbidv 2436 . . . . . . . 8 (𝑢 = 𝑗 → (∃𝑤 (2nd𝐴)𝑤 <Q 𝑢 ↔ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑗))
7271elrab 2835 . . . . . . 7 (𝑗 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢} ↔ (𝑗Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑗))
7369, 72syl6bb 195 . . . . . 6 (𝜑 → (𝑗 ∈ (2nd𝐵) ↔ (𝑗Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑗)))
7473rexbidv 2436 . . . . 5 (𝜑 → (∃𝑗Q 𝑗 ∈ (2nd𝐵) ↔ ∃𝑗Q (𝑗Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑗)))
7574adantr 274 . . . 4 ((𝜑 ∧ (𝑠Q𝑠 (2nd𝐴))) → (∃𝑗Q 𝑗 ∈ (2nd𝐵) ↔ ∃𝑗Q (𝑗Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑗)))
7665, 75mpbird 166 . . 3 ((𝜑 ∧ (𝑠Q𝑠 (2nd𝐴))) → ∃𝑗Q 𝑗 ∈ (2nd𝐵))
7745, 76rexlimddv 2552 . 2 (𝜑 → ∃𝑗Q 𝑗 ∈ (2nd𝐵))
78 eleq1w 2198 . . 3 (𝑗 = 𝑠 → (𝑗 ∈ (2nd𝐵) ↔ 𝑠 ∈ (2nd𝐵)))
7978cbvrexv 2653 . 2 (∃𝑗Q 𝑗 ∈ (2nd𝐵) ↔ ∃𝑠Q 𝑠 ∈ (2nd𝐵))
8077, 79sylib 121 1 (𝜑 → ∃𝑠Q 𝑠 ∈ (2nd𝐵))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → 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   Or wor 4212   “ cima 4537  Fun wfun 5112  –onto→wfo 5116  ‘cfv 5118  (class class class)co 5767  1st c1st 6029  2nd c2nd 6030  Qcnq 7081  1Qc1q 7082   +Q cplq 7083
 Copyright terms: Public domain W3C validator