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

Theorem caucvgprprlemell 7007
 Description: Lemma for caucvgprpr 7034. Membership in the lower cut of the putative limit. (Contributed by Jim Kingdon, 21-Jan-2021.)
Hypothesis
Ref Expression
caucvgprprlemell.lim 𝐿 = ⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩
Assertion
Ref Expression
caucvgprprlemell (𝑋 ∈ (1st𝐿) ↔ (𝑋Q ∧ ∃𝑏N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
Distinct variable groups:   𝐹,𝑏   𝐹,𝑙,𝑟   𝑢,𝐹,𝑟   𝑋,𝑏,𝑝   𝑋,𝑙,𝑟,𝑝   𝑢,𝑋,𝑝   𝑋,𝑞,𝑏   𝑞,𝑙,𝑟   𝑢,𝑞
Allowed substitution hints:   𝐹(𝑞,𝑝)   𝐿(𝑢,𝑟,𝑞,𝑝,𝑏,𝑙)

Proof of Theorem caucvgprprlemell
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 oveq1 5571 . . . . . . . 8 (𝑙 = 𝑋 → (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) = (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )))
21breq2d 3817 . . . . . . 7 (𝑙 = 𝑋 → (𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) ↔ 𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))))
32abbidv 2200 . . . . . 6 (𝑙 = 𝑋 → {𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))} = {𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))})
41breq1d 3815 . . . . . . 7 (𝑙 = 𝑋 → ((𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞 ↔ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞))
54abbidv 2200 . . . . . 6 (𝑙 = 𝑋 → {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞} = {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞})
63, 5opeq12d 3598 . . . . 5 (𝑙 = 𝑋 → ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩)
76breq1d 3815 . . . 4 (𝑙 = 𝑋 → (⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟) ↔ ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)))
87rexbidv 2374 . . 3 (𝑙 = 𝑋 → (∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟) ↔ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)))
9 caucvgprprlemell.lim . . . . 5 𝐿 = ⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩
109fveq2i 5233 . . . 4 (1st𝐿) = (1st ‘⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩)
11 nqex 6685 . . . . . 6 Q ∈ V
1211rabex 3942 . . . . 5 {𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)} ∈ V
1311rabex 3942 . . . . 5 {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩} ∈ V
1412, 13op1st 5825 . . . 4 (1st ‘⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩) = {𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}
1510, 14eqtri 2103 . . 3 (1st𝐿) = {𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}
168, 15elrab2 2760 . 2 (𝑋 ∈ (1st𝐿) ↔ (𝑋Q ∧ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)))
17 opeq1 3590 . . . . . . . . . . . 12 (𝑟 = 𝑎 → ⟨𝑟, 1𝑜⟩ = ⟨𝑎, 1𝑜⟩)
1817eceq1d 6230 . . . . . . . . . . 11 (𝑟 = 𝑎 → [⟨𝑟, 1𝑜⟩] ~Q = [⟨𝑎, 1𝑜⟩] ~Q )
1918fveq2d 5234 . . . . . . . . . 10 (𝑟 = 𝑎 → (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))
2019oveq2d 5580 . . . . . . . . 9 (𝑟 = 𝑎 → (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) = (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )))
2120breq2d 3817 . . . . . . . 8 (𝑟 = 𝑎 → (𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) ↔ 𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))))
2221abbidv 2200 . . . . . . 7 (𝑟 = 𝑎 → {𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))} = {𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))})
2320breq1d 3815 . . . . . . . 8 (𝑟 = 𝑎 → ((𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞 ↔ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞))
2423abbidv 2200 . . . . . . 7 (𝑟 = 𝑎 → {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞} = {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞})
2522, 24opeq12d 3598 . . . . . 6 (𝑟 = 𝑎 → ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞}⟩)
26 fveq2 5230 . . . . . 6 (𝑟 = 𝑎 → (𝐹𝑟) = (𝐹𝑎))
2725, 26breq12d 3818 . . . . 5 (𝑟 = 𝑎 → (⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟) ↔ ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎)))
2827cbvrexv 2583 . . . 4 (∃𝑟N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟) ↔ ∃𝑎N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎))
29 opeq1 3590 . . . . . . . . . . . 12 (𝑎 = 𝑏 → ⟨𝑎, 1𝑜⟩ = ⟨𝑏, 1𝑜⟩)
3029eceq1d 6230 . . . . . . . . . . 11 (𝑎 = 𝑏 → [⟨𝑎, 1𝑜⟩] ~Q = [⟨𝑏, 1𝑜⟩] ~Q )
3130fveq2d 5234 . . . . . . . . . 10 (𝑎 = 𝑏 → (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))
3231oveq2d 5580 . . . . . . . . 9 (𝑎 = 𝑏 → (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) = (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )))
3332breq2d 3817 . . . . . . . 8 (𝑎 = 𝑏 → (𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) ↔ 𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))))
3433abbidv 2200 . . . . . . 7 (𝑎 = 𝑏 → {𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))} = {𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))})
3532breq1d 3815 . . . . . . . 8 (𝑎 = 𝑏 → ((𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞 ↔ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞))
3635abbidv 2200 . . . . . . 7 (𝑎 = 𝑏 → {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞} = {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞})
3734, 36opeq12d 3598 . . . . . 6 (𝑎 = 𝑏 → ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩)
38 fveq2 5230 . . . . . 6 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
3937, 38breq12d 3818 . . . . 5 (𝑎 = 𝑏 → (⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎) ↔ ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
4039cbvrexv 2583 . . . 4 (∃𝑎N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎) ↔ ∃𝑏N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
4128, 40bitri 182 . . 3 (∃𝑟N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟) ↔ ∃𝑏N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
4241anbi2i 445 . 2 ((𝑋Q ∧ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)) ↔ (𝑋Q ∧ ∃𝑏N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
4316, 42bitri 182 1 (𝑋 ∈ (1st𝐿) ↔ (𝑋Q ∧ ∃𝑏N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
 Colors of variables: wff set class Syntax hints:   ∧ wa 102   ↔ wb 103   = wceq 1285   ∈ wcel 1434  {cab 2069  ∃wrex 2354  {crab 2357  ⟨cop 3419   class class class wbr 3805  ‘cfv 4952  (class class class)co 5564  1st c1st 5817  1𝑜c1o 6079  [cec 6192  Ncnpi 6594   ~Q ceq 6601  Qcnq 6602   +Q cplq 6604  *Qcrq 6606
 Copyright terms: Public domain W3C validator