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

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

Proof of Theorem recexprlemell
StepHypRef Expression
1 elex 2692 . 2 (𝐶 ∈ (1st𝐵) → 𝐶 ∈ V)
2 ltrelnq 7166 . . . . . . 7 <Q ⊆ (Q × Q)
32brel 4586 . . . . . 6 (𝐶 <Q 𝑦 → (𝐶Q𝑦Q))
43simpld 111 . . . . 5 (𝐶 <Q 𝑦𝐶Q)
5 elex 2692 . . . . 5 (𝐶Q𝐶 ∈ V)
64, 5syl 14 . . . 4 (𝐶 <Q 𝑦𝐶 ∈ V)
76adantr 274 . . 3 ((𝐶 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → 𝐶 ∈ V)
87exlimiv 1577 . 2 (∃𝑦(𝐶 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → 𝐶 ∈ V)
9 breq1 3927 . . . . 5 (𝑥 = 𝐶 → (𝑥 <Q 𝑦𝐶 <Q 𝑦))
109anbi1d 460 . . . 4 (𝑥 = 𝐶 → ((𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) ↔ (𝐶 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))))
1110exbidv 1797 . . 3 (𝑥 = 𝐶 → (∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) ↔ ∃𝑦(𝐶 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))))
12 recexpr.1 . . . . 5 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
1312fveq2i 5417 . . . 4 (1st𝐵) = (1st ‘⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩)
14 nqex 7164 . . . . . 6 Q ∈ V
152brel 4586 . . . . . . . . . 10 (𝑥 <Q 𝑦 → (𝑥Q𝑦Q))
1615simpld 111 . . . . . . . . 9 (𝑥 <Q 𝑦𝑥Q)
1716adantr 274 . . . . . . . 8 ((𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → 𝑥Q)
1817exlimiv 1577 . . . . . . 7 (∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → 𝑥Q)
1918abssi 3167 . . . . . 6 {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))} ⊆ Q
2014, 19ssexi 4061 . . . . 5 {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))} ∈ V
212brel 4586 . . . . . . . . . 10 (𝑦 <Q 𝑥 → (𝑦Q𝑥Q))
2221simprd 113 . . . . . . . . 9 (𝑦 <Q 𝑥𝑥Q)
2322adantr 274 . . . . . . . 8 ((𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴)) → 𝑥Q)
2423exlimiv 1577 . . . . . . 7 (∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴)) → 𝑥Q)
2524abssi 3167 . . . . . 6 {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))} ⊆ Q
2614, 25ssexi 4061 . . . . 5 {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))} ∈ V
2720, 26op1st 6037 . . . 4 (1st ‘⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩) = {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}
2813, 27eqtri 2158 . . 3 (1st𝐵) = {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}
2911, 28elab2g 2826 . 2 (𝐶 ∈ V → (𝐶 ∈ (1st𝐵) ↔ ∃𝑦(𝐶 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))))
301, 8, 29pm5.21nii 693 1 (𝐶 ∈ (1st𝐵) ↔ ∃𝑦(𝐶 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1331  ∃wex 1468   ∈ wcel 1480  {cab 2123  Vcvv 2681  ⟨cop 3525   class class class wbr 3924  ‘cfv 5118  1st c1st 6029  2nd c2nd 6030  Qcnq 7081  *Qcrq 7085
 Copyright terms: Public domain W3C validator