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

Theorem recexprlemelu 6721
 Description: Membership in the upper cut of 𝐵. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.)
Hypothesis
Ref Expression
recexpr.1 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
Assertion
Ref Expression
recexprlemelu (𝐶 ∈ (2nd𝐵) ↔ ∃𝑦(𝑦 <Q 𝐶 ∧ (*Q𝑦) ∈ (1st𝐴)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦

Proof of Theorem recexprlemelu
StepHypRef Expression
1 elex 2566 . 2 (𝐶 ∈ (2nd𝐵) → 𝐶 ∈ V)
2 ltrelnq 6463 . . . . . . 7 <Q ⊆ (Q × Q)
32brel 4392 . . . . . 6 (𝑦 <Q 𝐶 → (𝑦Q𝐶Q))
43simprd 107 . . . . 5 (𝑦 <Q 𝐶𝐶Q)
5 elex 2566 . . . . 5 (𝐶Q𝐶 ∈ V)
64, 5syl 14 . . . 4 (𝑦 <Q 𝐶𝐶 ∈ V)
76adantr 261 . . 3 ((𝑦 <Q 𝐶 ∧ (*Q𝑦) ∈ (1st𝐴)) → 𝐶 ∈ V)
87exlimiv 1489 . 2 (∃𝑦(𝑦 <Q 𝐶 ∧ (*Q𝑦) ∈ (1st𝐴)) → 𝐶 ∈ V)
9 breq2 3768 . . . . 5 (𝑥 = 𝐶 → (𝑦 <Q 𝑥𝑦 <Q 𝐶))
109anbi1d 438 . . . 4 (𝑥 = 𝐶 → ((𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴)) ↔ (𝑦 <Q 𝐶 ∧ (*Q𝑦) ∈ (1st𝐴))))
1110exbidv 1706 . . 3 (𝑥 = 𝐶 → (∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴)) ↔ ∃𝑦(𝑦 <Q 𝐶 ∧ (*Q𝑦) ∈ (1st𝐴))))
12 recexpr.1 . . . . 5 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
1312fveq2i 5181 . . . 4 (2nd𝐵) = (2nd ‘⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩)
14 nqex 6461 . . . . . 6 Q ∈ V
152brel 4392 . . . . . . . . . 10 (𝑥 <Q 𝑦 → (𝑥Q𝑦Q))
1615simpld 105 . . . . . . . . 9 (𝑥 <Q 𝑦𝑥Q)
1716adantr 261 . . . . . . . 8 ((𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → 𝑥Q)
1817exlimiv 1489 . . . . . . 7 (∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → 𝑥Q)
1918abssi 3015 . . . . . 6 {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))} ⊆ Q
2014, 19ssexi 3895 . . . . 5 {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))} ∈ V
212brel 4392 . . . . . . . . . 10 (𝑦 <Q 𝑥 → (𝑦Q𝑥Q))
2221simprd 107 . . . . . . . . 9 (𝑦 <Q 𝑥𝑥Q)
2322adantr 261 . . . . . . . 8 ((𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴)) → 𝑥Q)
2423exlimiv 1489 . . . . . . 7 (∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴)) → 𝑥Q)
2524abssi 3015 . . . . . 6 {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))} ⊆ Q
2614, 25ssexi 3895 . . . . 5 {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))} ∈ V
2720, 26op2nd 5774 . . . 4 (2nd ‘⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩) = {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}
2813, 27eqtri 2060 . . 3 (2nd𝐵) = {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}
2911, 28elab2g 2689 . 2 (𝐶 ∈ V → (𝐶 ∈ (2nd𝐵) ↔ ∃𝑦(𝑦 <Q 𝐶 ∧ (*Q𝑦) ∈ (1st𝐴))))
301, 8, 29pm5.21nii 620 1 (𝐶 ∈ (2nd𝐵) ↔ ∃𝑦(𝑦 <Q 𝐶 ∧ (*Q𝑦) ∈ (1st𝐴)))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98   = wceq 1243  ∃wex 1381   ∈ wcel 1393  {cab 2026  Vcvv 2557  ⟨cop 3378   class class class wbr 3764  ‘cfv 4902  1st c1st 5765  2nd c2nd 5766  Qcnq 6378  *Qcrq 6382
 Copyright terms: Public domain W3C validator