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

Theorem suplocexprlem2b 7522
 Description: Lemma for suplocexpr 7533. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.)
Hypothesis
Ref Expression
suplocexprlem2b.b 𝐵 = ⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩
Assertion
Ref Expression
suplocexprlem2b (𝐴P → (2nd𝐵) = {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})

Proof of Theorem suplocexprlem2b
StepHypRef Expression
1 suplocexprlem2b.b . . 3 𝐵 = ⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩
21fveq2i 5424 . 2 (2nd𝐵) = (2nd ‘⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩)
3 fo1st 6055 . . . . . 6 1st :V–onto→V
4 fofun 5346 . . . . . 6 (1st :V–onto→V → Fun 1st )
53, 4ax-mp 5 . . . . 5 Fun 1st
6 npex 7281 . . . . . 6 P ∈ V
76ssex 4065 . . . . 5 (𝐴P𝐴 ∈ V)
8 funimaexg 5207 . . . . 5 ((Fun 1st𝐴 ∈ V) → (1st𝐴) ∈ V)
95, 7, 8sylancr 410 . . . 4 (𝐴P → (1st𝐴) ∈ V)
10 uniexg 4361 . . . 4 ((1st𝐴) ∈ V → (1st𝐴) ∈ V)
119, 10syl 14 . . 3 (𝐴P (1st𝐴) ∈ V)
12 nqex 7171 . . . 4 Q ∈ V
1312rabex 4072 . . 3 {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢} ∈ V
14 op2ndg 6049 . . 3 (( (1st𝐴) ∈ V ∧ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢} ∈ V) → (2nd ‘⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩) = {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
1511, 13, 14sylancl 409 . 2 (𝐴P → (2nd ‘⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩) = {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
162, 15syl5eq 2184 1 (𝐴P → (2nd𝐵) = {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480  ∃wrex 2417  {crab 2420  Vcvv 2686   ⊆ wss 3071  ⟨cop 3530  ∪ cuni 3736  ∩ cint 3771   class class class wbr 3929   “ cima 4542  Fun wfun 5117  –onto→wfo 5121  ‘cfv 5123  1st c1st 6036  2nd c2nd 6037  Qcnq 7088
 Copyright terms: Public domain W3C validator