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

Theorem caucvgprprlemlol 7631
Description: Lemma for caucvgprpr 7645. 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‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))))
caucvgprpr.bnd (𝜑 → ∀𝑚N 𝐴<P (𝐹𝑚))
caucvgprpr.lim 𝐿 = ⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~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 7298 . . . . 5 <Q ⊆ (Q × Q)
21brel 4651 . . . 4 (𝑠 <Q 𝑡 → (𝑠Q𝑡Q))
32simpld 111 . . 3 (𝑠 <Q 𝑡𝑠Q)
433ad2ant2 1008 . 2 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑠Q)
5 caucvgprpr.lim . . . . . . 7 𝐿 = ⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩
65caucvgprprlemell 7618 . . . . . 6 (𝑡 ∈ (1st𝐿) ↔ (𝑡Q ∧ ∃𝑏N ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
76simprbi 273 . . . . 5 (𝑡 ∈ (1st𝐿) → ∃𝑏N ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
873ad2ant3 1009 . . . 4 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → ∃𝑏N ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
9 simpll2 1026 . . . . . . . . 9 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → 𝑠 <Q 𝑡)
10 ltanqg 7333 . . . . . . . . . . 11 ((𝑥Q𝑦Q𝑧Q) → (𝑥 <Q 𝑦 ↔ (𝑧 +Q 𝑥) <Q (𝑧 +Q 𝑦)))
1110adantl 275 . . . . . . . . . 10 (((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) ∧ (𝑥Q𝑦Q𝑧Q)) → (𝑥 <Q 𝑦 ↔ (𝑧 +Q 𝑥) <Q (𝑧 +Q 𝑦)))
124ad2antrr 480 . . . . . . . . . 10 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → 𝑠Q)
132simprd 113 . . . . . . . . . . . 12 (𝑠 <Q 𝑡𝑡Q)
14133ad2ant2 1008 . . . . . . . . . . 11 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑡Q)
1514ad2antrr 480 . . . . . . . . . 10 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → 𝑡Q)
16 simplr 520 . . . . . . . . . . 11 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → 𝑏N)
17 nnnq 7355 . . . . . . . . . . 11 (𝑏N → [⟨𝑏, 1o⟩] ~QQ)
18 recclnq 7325 . . . . . . . . . . 11 ([⟨𝑏, 1o⟩] ~QQ → (*Q‘[⟨𝑏, 1o⟩] ~Q ) ∈ Q)
1916, 17, 183syl 17 . . . . . . . . . 10 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → (*Q‘[⟨𝑏, 1o⟩] ~Q ) ∈ Q)
20 addcomnqg 7314 . . . . . . . . . . 11 ((𝑥Q𝑦Q) → (𝑥 +Q 𝑦) = (𝑦 +Q 𝑥))
2120adantl 275 . . . . . . . . . 10 (((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) ∧ (𝑥Q𝑦Q)) → (𝑥 +Q 𝑦) = (𝑦 +Q 𝑥))
2211, 12, 15, 19, 21caovord2d 6003 . . . . . . . . 9 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → (𝑠 <Q 𝑡 ↔ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))))
239, 22mpbid 146 . . . . . . . 8 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )))
24 ltnqpri 7527 . . . . . . . 8 ((𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩)
2523, 24syl 14 . . . . . . 7 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩)
26 ltsopr 7529 . . . . . . . 8 <P Or P
27 ltrelpr 7438 . . . . . . . 8 <P ⊆ (P × P)
2826, 27sotri 4994 . . . . . . 7 ((⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩ ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
2925, 28sylancom 417 . . . . . 6 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
3029ex 114 . . . . 5 (((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) → (⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
3130reximdva 2566 . . . 4 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → (∃𝑏N ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏) → ∃𝑏N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
328, 31mpd 13 . . 3 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → ∃𝑏N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
33 opeq1 3753 . . . . . . . . . . 11 (𝑏 = 𝑟 → ⟨𝑏, 1o⟩ = ⟨𝑟, 1o⟩)
3433eceq1d 6529 . . . . . . . . . 10 (𝑏 = 𝑟 → [⟨𝑏, 1o⟩] ~Q = [⟨𝑟, 1o⟩] ~Q )
3534fveq2d 5485 . . . . . . . . 9 (𝑏 = 𝑟 → (*Q‘[⟨𝑏, 1o⟩] ~Q ) = (*Q‘[⟨𝑟, 1o⟩] ~Q ))
3635oveq2d 5853 . . . . . . . 8 (𝑏 = 𝑟 → (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) = (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )))
3736breq2d 3989 . . . . . . 7 (𝑏 = 𝑟 → (𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) ↔ 𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))))
3837abbidv 2282 . . . . . 6 (𝑏 = 𝑟 → {𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))} = {𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))})
3936breq1d 3987 . . . . . . 7 (𝑏 = 𝑟 → ((𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞 ↔ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞))
4039abbidv 2282 . . . . . 6 (𝑏 = 𝑟 → {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞} = {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞})
4138, 40opeq12d 3761 . . . . 5 (𝑏 = 𝑟 → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩)
42 fveq2 5481 . . . . 5 (𝑏 = 𝑟 → (𝐹𝑏) = (𝐹𝑟))
4341, 42breq12d 3990 . . . 4 (𝑏 = 𝑟 → (⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏) ↔ ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)))
4443cbvrexv 2691 . . 3 (∃𝑏N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏) ↔ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟))
4532, 44sylib 121 . 2 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → ∃𝑟N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟))
465caucvgprprlemell 7618 . 2 (𝑠 ∈ (1st𝐿) ↔ (𝑠Q ∧ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)))
474, 45, 46sylanbrc 414 1 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑠 ∈ (1st𝐿))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 967   = wceq 1342  wcel 2135  {cab 2150  wral 2442  wrex 2443  {crab 2446  cop 3574   class class class wbr 3977  wf 5179  cfv 5183  (class class class)co 5837  1st c1st 6099  1oc1o 6369  [cec 6491  Ncnpi 7205   <N clti 7208   ~Q ceq 7212  Qcnq 7213   +Q cplq 7215  *Qcrq 7217   <Q cltq 7218  Pcnp 7224   +P cpp 7226  <P cltp 7228
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-coll 4092  ax-sep 4095  ax-nul 4103  ax-pow 4148  ax-pr 4182  ax-un 4406  ax-setind 4509  ax-iinf 4560
This theorem depends on definitions:  df-bi 116  df-dc 825  df-3or 968  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-ral 2447  df-rex 2448  df-reu 2449  df-rab 2451  df-v 2724  df-sbc 2948  df-csb 3042  df-dif 3114  df-un 3116  df-in 3118  df-ss 3125  df-nul 3406  df-pw 3556  df-sn 3577  df-pr 3578  df-op 3580  df-uni 3785  df-int 3820  df-iun 3863  df-br 3978  df-opab 4039  df-mpt 4040  df-tr 4076  df-eprel 4262  df-id 4266  df-po 4269  df-iso 4270  df-iord 4339  df-on 4341  df-suc 4344  df-iom 4563  df-xp 4605  df-rel 4606  df-cnv 4607  df-co 4608  df-dm 4609  df-rn 4610  df-res 4611  df-ima 4612  df-iota 5148  df-fun 5185  df-fn 5186  df-f 5187  df-f1 5188  df-fo 5189  df-f1o 5190  df-fv 5191  df-ov 5840  df-oprab 5841  df-mpo 5842  df-1st 6101  df-2nd 6102  df-recs 6265  df-irdg 6330  df-1o 6376  df-oadd 6380  df-omul 6381  df-er 6493  df-ec 6495  df-qs 6499  df-ni 7237  df-pli 7238  df-mi 7239  df-lti 7240  df-plpq 7277  df-mpq 7278  df-enq 7280  df-nqqs 7281  df-plqqs 7282  df-mqqs 7283  df-1nqqs 7284  df-rq 7285  df-ltnqqs 7286  df-inp 7399  df-iltp 7403
This theorem is referenced by:  caucvgprprlemrnd  7634
  Copyright terms: Public domain W3C validator