Theorem axcaucvglemval 6971

Description: Lemma for axcaucvg 6974. Value of sequence when mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.)

Hypotheses

Ref	Expression
axcaucvg.n	⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
axcaucvg.f	⊢ (𝜑 → 𝐹:𝑁⟶ℝ)
axcaucvg.cau	⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))
axcaucvg.g	⊢ 𝐺 = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))

Assertion

Ref	Expression
axcaucvglemval	⊢ ((𝜑 ∧ 𝐽 ∈ N) → (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨(𝐺‘𝐽), 0R⟩)

Distinct variable groups:   𝑗,𝐹,𝑧   𝑧,𝐺   𝑗,𝐽,𝑙,𝑢,𝑧   𝜑,𝑗   𝑦,𝑙,𝑢   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑢,𝑘,𝑛,𝑟,𝑙)   𝐹(𝑥,𝑦,𝑢,𝑘,𝑛,𝑟,𝑙)   𝐺(𝑥,𝑦,𝑢,𝑗,𝑘,𝑛,𝑟,𝑙)   𝐽(𝑥,𝑦,𝑘,𝑛,𝑟)   𝑁(𝑥,𝑦,𝑧,𝑢,𝑗,𝑘,𝑛,𝑟,𝑙)

Proof of Theorem axcaucvglemval

Step	Hyp	Ref	Expression
1		axcaucvg.g	. . . . 5 ⊢ 𝐺 = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))
2	1	a1i 9	. . . 4 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → 𝐺 = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩)))
3		opeq1 3549	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → ⟨𝑗, 1𝑜⟩ = ⟨𝐽, 1𝑜⟩)
4	3	eceq1d 6142	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → [⟨𝑗, 1𝑜⟩] ~Q = [⟨𝐽, 1𝑜⟩] ~Q )
5	4	breq2d 3776	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐽 → (𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q ↔ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q ))
6	5	abbidv 2155	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐽 → {𝑙 ∣ 𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q } = {𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q })
7	4	breq1d 3774	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐽 → ([⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢 ↔ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢))
8	7	abbidv 2155	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐽 → {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢} = {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢})
9	6, 8	opeq12d 3557	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐽 → ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩)
10	9	oveq1d 5527	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐽 → (⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) = (⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P))
11	10	opeq1d 3555	. . . . . . . . . 10 ⊢ (𝑗 = 𝐽 → ⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩ = ⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩)
12	11	eceq1d 6142	. . . . . . . . 9 ⊢ (𝑗 = 𝐽 → [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R = [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
13	12	opeq1d 3555	. . . . . . . 8 ⊢ (𝑗 = 𝐽 → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ = ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
14	13	fveq2d 5182	. . . . . . 7 ⊢ (𝑗 = 𝐽 → (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩))
15	14	eqeq1d 2048	. . . . . 6 ⊢ (𝑗 = 𝐽 → ((𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩ ↔ (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))
16	15	riotabidv 5470	. . . . 5 ⊢ (𝑗 = 𝐽 → (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) = (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))
17	16	adantl 262	. . . 4 ⊢ (((𝜑 ∧ 𝐽 ∈ N) ∧ 𝑗 = 𝐽) → (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) = (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))
18		simpr 103	. . . 4 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → 𝐽 ∈ N)
19		axcaucvg.n	. . . . 5 ⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
20		axcaucvg.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝑁⟶ℝ)
21	19, 20	axcaucvglemcl 6969	. . . 4 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) ∈ R)
22	2, 17, 18, 21	fvmptd 5253	. . 3 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (𝐺‘𝐽) = (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))
23	22	eqcomd 2045	. 2 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) = (𝐺‘𝐽))
24	22, 21	eqeltrd 2114	. . 3 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (𝐺‘𝐽) ∈ R)
25	20	adantr 261	. . . . . 6 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → 𝐹:𝑁⟶ℝ)
26		pitonn 6924	. . . . . . . 8 ⊢ (𝐽 ∈ N → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
27	26, 19	syl6eleqr 2131	. . . . . . 7 ⊢ (𝐽 ∈ N → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ 𝑁)
28	27	adantl 262	. . . . . 6 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ 𝑁)
29	25, 28	ffvelrnd 5303	. . . . 5 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) ∈ ℝ)
30		elrealeu 6906	. . . . 5 ⊢ ((𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) ∈ ℝ ↔ ∃!𝑧 ∈ R ⟨𝑧, 0R⟩ = (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩))
31	29, 30	sylib 127	. . . 4 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → ∃!𝑧 ∈ R ⟨𝑧, 0R⟩ = (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩))
32		eqcom 2042	. . . . 5 ⊢ (⟨𝑧, 0R⟩ = (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) ↔ (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩)
33	32	reubii 2495	. . . 4 ⊢ (∃!𝑧 ∈ R ⟨𝑧, 0R⟩ = (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) ↔ ∃!𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩)
34	31, 33	sylib 127	. . 3 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → ∃!𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩)
35		opeq1 3549	. . . . 5 ⊢ (𝑧 = (𝐺‘𝐽) → ⟨𝑧, 0R⟩ = ⟨(𝐺‘𝐽), 0R⟩)
36	35	eqeq2d 2051	. . . 4 ⊢ (𝑧 = (𝐺‘𝐽) → ((𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩ ↔ (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨(𝐺‘𝐽), 0R⟩))
37	36	riota2 5490	. . 3 ⊢ (((𝐺‘𝐽) ∈ R ∧ ∃!𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) → ((𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨(𝐺‘𝐽), 0R⟩ ↔ (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) = (𝐺‘𝐽)))
38	24, 34, 37	syl2anc 391	. 2 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → ((𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨(𝐺‘𝐽), 0R⟩ ↔ (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) = (𝐺‘𝐽)))
39	23, 38	mpbird 156	1 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨(𝐺‘𝐽), 0R⟩)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1243   ∈ wcel 1393  {cab 2026  ∀wral 2306  ∃!wreu 2308  ⟨cop 3378  ∩ cint 3615   class class class wbr 3764   ↦ cmpt 3818  ⟶wf 4898  ‘cfv 4902  ℩crio 5467  (class class class)co 5512  1_𝑜c1o 5994  [cec 6104  Ncnpi 6370   ~_Q ceq 6377   <_Q cltq 6383  1_Pc1p 6390   +_P cpp 6391   ~_R cer 6394  Rcnr 6395  0_Rc0r 6396  ℝcr 6888  1c1 6890   + caddc 6892   <_ℝ cltrr 6893   · cmul 6894

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-coll 3872  ax-sep 3875  ax-nul 3883  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-setind 4262  ax-iinf 4311

This theorem depends on definitions:  df-bi 110  df-dc 743  df-3or 886  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-ral 2311  df-rex 2312  df-reu 2313  df-rmo 2314  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-int 3616  df-iun 3659  df-br 3765  df-opab 3819  df-mpt 3820  df-tr 3855  df-eprel 4026  df-id 4030  df-po 4033  df-iso 4034  df-iord 4103  df-on 4105  df-suc 4108  df-iom 4314  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909  df-fv 4910  df-riota 5468  df-ov 5515  df-oprab 5516  df-mpt2 5517  df-1st 5767  df-2nd 5768  df-recs 5920  df-irdg 5957  df-1o 6001  df-2o 6002  df-oadd 6005  df-omul 6006  df-er 6106  df-ec 6108  df-qs 6112  df-ni 6402  df-pli 6403  df-mi 6404  df-lti 6405  df-plpq 6442  df-mpq 6443  df-enq 6445  df-nqqs 6446  df-plqqs 6447  df-mqqs 6448  df-1nqqs 6449  df-rq 6450  df-ltnqqs 6451  df-enq0 6522  df-nq0 6523  df-0nq0 6524  df-plq0 6525  df-mq0 6526  df-inp 6564  df-i1p 6565  df-iplp 6566  df-enr 6811  df-nr 6812  df-plr 6813  df-0r 6816  df-1r 6817  df-c 6895  df-1 6897  df-r 6899  df-add 6900

This theorem is referenced by:  axcaucvglemcau  6972  axcaucvglemres  6973