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

Theorem caucvgprprlemlol 6853
 Description: Lemma for caucvgprpr 6867. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 21-Dec-2020.)
Hypotheses
Ref Expression
caucvgprpr.f (𝜑𝐹:NP)
caucvgprpr.cau (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
caucvgprpr.bnd (𝜑 → ∀𝑚N 𝐴<P (𝐹𝑚))
caucvgprpr.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
caucvgprprlemlol ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑠 ∈ (1st𝐿))
Distinct variable groups:   𝐴,𝑚   𝑚,𝐹   𝐹,𝑙   𝑢,𝐹,𝑟   𝑝,𝑙,𝑠   𝑞,𝑙,𝑠,𝑟   𝑡,𝑙,𝑝   𝑢,𝑞,𝑠,𝑟   𝑢,𝑝,𝑡,𝑟   𝜑,𝑟   𝑟,𝑞,𝑡
Allowed substitution hints:   𝜑(𝑢,𝑡,𝑘,𝑚,𝑛,𝑠,𝑞,𝑝,𝑙)   𝐴(𝑢,𝑡,𝑘,𝑛,𝑠,𝑟,𝑞,𝑝,𝑙)   𝐹(𝑡,𝑘,𝑛,𝑠,𝑞,𝑝)   𝐿(𝑢,𝑡,𝑘,𝑚,𝑛,𝑠,𝑟,𝑞,𝑝,𝑙)

Proof of Theorem caucvgprprlemlol
Dummy variables 𝑏 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelnq 6520 . . . . 5 <Q ⊆ (Q × Q)
21brel 4419 . . . 4 (𝑠 <Q 𝑡 → (𝑠Q𝑡Q))
32simpld 109 . . 3 (𝑠 <Q 𝑡𝑠Q)
433ad2ant2 937 . 2 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑠Q)
5 caucvgprpr.lim . . . . . . 7 𝐿 = ⟨{𝑙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 𝑞}⟩}⟩
65caucvgprprlemell 6840 . . . . . 6 (𝑡 ∈ (1st𝐿) ↔ (𝑡Q ∧ ∃𝑏N ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
76simprbi 264 . . . . 5 (𝑡 ∈ (1st𝐿) → ∃𝑏N ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
873ad2ant3 938 . . . 4 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → ∃𝑏N ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
9 simpll2 955 . . . . . . . . 9 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → 𝑠 <Q 𝑡)
10 ltanqg 6555 . . . . . . . . . . 11 ((𝑥Q𝑦Q𝑧Q) → (𝑥 <Q 𝑦 ↔ (𝑧 +Q 𝑥) <Q (𝑧 +Q 𝑦)))
1110adantl 266 . . . . . . . . . 10 (((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) ∧ (𝑥Q𝑦Q𝑧Q)) → (𝑥 <Q 𝑦 ↔ (𝑧 +Q 𝑥) <Q (𝑧 +Q 𝑦)))
124ad2antrr 465 . . . . . . . . . 10 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → 𝑠Q)
132simprd 111 . . . . . . . . . . . 12 (𝑠 <Q 𝑡𝑡Q)
14133ad2ant2 937 . . . . . . . . . . 11 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑡Q)
1514ad2antrr 465 . . . . . . . . . 10 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → 𝑡Q)
16 simplr 490 . . . . . . . . . . 11 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → 𝑏N)
17 nnnq 6577 . . . . . . . . . . 11 (𝑏N → [⟨𝑏, 1𝑜⟩] ~QQ)
18 recclnq 6547 . . . . . . . . . . 11 ([⟨𝑏, 1𝑜⟩] ~QQ → (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) ∈ Q)
1916, 17, 183syl 17 . . . . . . . . . 10 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) ∈ Q)
20 addcomnqg 6536 . . . . . . . . . . 11 ((𝑥Q𝑦Q) → (𝑥 +Q 𝑦) = (𝑦 +Q 𝑥))
2120adantl 266 . . . . . . . . . 10 (((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) ∧ (𝑥Q𝑦Q)) → (𝑥 +Q 𝑦) = (𝑦 +Q 𝑥))
2211, 12, 15, 19, 21caovord2d 5697 . . . . . . . . 9 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → (𝑠 <Q 𝑡 ↔ (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))))
239, 22mpbid 139 . . . . . . . 8 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )))
24 ltnqpri 6749 . . . . . . . 8 ((𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩)
2523, 24syl 14 . . . . . . 7 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩)
26 ltsopr 6751 . . . . . . . 8 <P Or P
27 ltrelpr 6660 . . . . . . . 8 <P ⊆ (P × P)
2826, 27sotri 4747 . . . . . . 7 ((⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩ ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
2925, 28sylancom 405 . . . . . 6 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
3029ex 112 . . . . 5 (((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) → (⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
3130reximdva 2438 . . . 4 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → (∃𝑏N ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏) → ∃𝑏N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
328, 31mpd 13 . . 3 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → ∃𝑏N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
33 opeq1 3576 . . . . . . . . . . 11 (𝑏 = 𝑟 → ⟨𝑏, 1𝑜⟩ = ⟨𝑟, 1𝑜⟩)
3433eceq1d 6172 . . . . . . . . . 10 (𝑏 = 𝑟 → [⟨𝑏, 1𝑜⟩] ~Q = [⟨𝑟, 1𝑜⟩] ~Q )
3534fveq2d 5209 . . . . . . . . 9 (𝑏 = 𝑟 → (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))
3635oveq2d 5555 . . . . . . . 8 (𝑏 = 𝑟 → (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) = (𝑠 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )))
3736breq2d 3803 . . . . . . 7 (𝑏 = 𝑟 → (𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) ↔ 𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))))
3837abbidv 2171 . . . . . 6 (𝑏 = 𝑟 → {𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))} = {𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))})
3936breq1d 3801 . . . . . . 7 (𝑏 = 𝑟 → ((𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞 ↔ (𝑠 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞))
4039abbidv 2171 . . . . . 6 (𝑏 = 𝑟 → {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞} = {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞})
4138, 40opeq12d 3584 . . . . 5 (𝑏 = 𝑟 → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩)
42 fveq2 5205 . . . . 5 (𝑏 = 𝑟 → (𝐹𝑏) = (𝐹𝑟))
4341, 42breq12d 3804 . . . 4 (𝑏 = 𝑟 → (⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏) ↔ ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)))
4443cbvrexv 2551 . . 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 (𝐹𝑟))
4532, 44sylib 131 . 2 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → ∃𝑟N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟))
465caucvgprprlemell 6840 . 2 (𝑠 ∈ (1st𝐿) ↔ (𝑠Q ∧ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)))
474, 45, 46sylanbrc 402 1 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑠 ∈ (1st𝐿))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   ∧ w3a 896   = wceq 1259   ∈ wcel 1409  {cab 2042  ∀wral 2323  ∃wrex 2324  {crab 2327  ⟨cop 3405   class class class wbr 3791  ⟶wf 4925  ‘cfv 4929  (class class class)co 5539  1st c1st 5792  1𝑜c1o 6024  [cec 6134  Ncnpi 6427
 Copyright terms: Public domain W3C validator