Theorem pitonnlem2 7438

Description: Lemma for pitonn 7439. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.)

Assertion

Ref	Expression
pitonnlem2	⊢ (𝐾 ∈ N → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ + 1) = ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨(𝐾 +N 1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝐾 +N 1o), 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)

Distinct variable group:   𝐾,𝑙,𝑢

Proof of Theorem pitonnlem2

Step	Hyp	Ref	Expression
1		df-1 7412	. . . 4 ⊢ 1 = ⟨1R, 0R⟩
2	1	oveq2i 5677	. . 3 ⊢ (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ + 1) = (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ + ⟨1R, 0R⟩)
3		nnprlu 7166	. . . . . . . 8 ⊢ (𝐾 ∈ N → ⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ ∈ P)
4		1pr 7167	. . . . . . . 8 ⊢ 1P ∈ P
5		addclpr 7150	. . . . . . . 8 ⊢ ((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ ∈ P ∧ 1P ∈ P) → (⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) ∈ P)
6	3, 4, 5	sylancl 405	. . . . . . 7 ⊢ (𝐾 ∈ N → (⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) ∈ P)
7		opelxpi 4482	. . . . . . 7 ⊢ (((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) ∈ P ∧ 1P ∈ P) → ⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩ ∈ (P × P))
8	6, 4, 7	sylancl 405	. . . . . 6 ⊢ (𝐾 ∈ N → ⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩ ∈ (P × P))
9		enrex 7337	. . . . . . 7 ⊢ ~R ∈ V
10	9	ecelqsi 6360	. . . . . 6 ⊢ (⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩ ∈ (P × P) → [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ∈ ((P × P) / ~R ))
11	8, 10	syl 14	. . . . 5 ⊢ (𝐾 ∈ N → [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ∈ ((P × P) / ~R ))
12		df-nr 7327	. . . . 5 ⊢ R = ((P × P) / ~R )
13	11, 12	syl6eleqr 2182	. . . 4 ⊢ (𝐾 ∈ N → [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ∈ R)
14		1sr 7351	. . . 4 ⊢ 1R ∈ R
15		addresr 7428	. . . 4 ⊢ (([⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ∈ R ∧ 1R ∈ R) → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ + ⟨1R, 0R⟩) = ⟨([⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R +R 1R), 0R⟩)
16	13, 14, 15	sylancl 405	. . 3 ⊢ (𝐾 ∈ N → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ + ⟨1R, 0R⟩) = ⟨([⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R +R 1R), 0R⟩)
17	2, 16	syl5eq 2133	. 2 ⊢ (𝐾 ∈ N → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ + 1) = ⟨([⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R +R 1R), 0R⟩)
18		pitonnlem1p1 7437	. . . . 5 ⊢ ((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) ∈ P → [⟨((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) +P (1P +P 1P)), (1P +P 1P)⟩] ~R = [⟨((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) +P 1P), 1P⟩] ~R )
19	6, 18	syl 14	. . . 4 ⊢ (𝐾 ∈ N → [⟨((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) +P (1P +P 1P)), (1P +P 1P)⟩] ~R = [⟨((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) +P 1P), 1P⟩] ~R )
20		df-1r 7332	. . . . . 6 ⊢ 1R = [⟨(1P +P 1P), 1P⟩] ~R
21	20	oveq2i 5677	. . . . 5 ⊢ ([⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R +R 1R) = ([⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R +R [⟨(1P +P 1P), 1P⟩] ~R )
22		addclpr 7150	. . . . . . . 8 ⊢ ((1P ∈ P ∧ 1P ∈ P) → (1P +P 1P) ∈ P)
23	4, 4, 22	mp2an 418	. . . . . . 7 ⊢ (1P +P 1P) ∈ P
24		addsrpr 7345	. . . . . . . 8 ⊢ ((((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) ∈ P ∧ 1P ∈ P) ∧ ((1P +P 1P) ∈ P ∧ 1P ∈ P)) → ([⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R +R [⟨(1P +P 1P), 1P⟩] ~R ) = [⟨((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) +P (1P +P 1P)), (1P +P 1P)⟩] ~R )
25	4, 24	mpanl2 427	. . . . . . 7 ⊢ (((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) ∈ P ∧ ((1P +P 1P) ∈ P ∧ 1P ∈ P)) → ([⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R +R [⟨(1P +P 1P), 1P⟩] ~R ) = [⟨((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) +P (1P +P 1P)), (1P +P 1P)⟩] ~R )
26	23, 4, 25	mpanr12 431	. . . . . 6 ⊢ ((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) ∈ P → ([⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R +R [⟨(1P +P 1P), 1P⟩] ~R ) = [⟨((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) +P (1P +P 1P)), (1P +P 1P)⟩] ~R )
27	6, 26	syl 14	. . . . 5 ⊢ (𝐾 ∈ N → ([⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R +R [⟨(1P +P 1P), 1P⟩] ~R ) = [⟨((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) +P (1P +P 1P)), (1P +P 1P)⟩] ~R )
28	21, 27	syl5eq 2133	. . . 4 ⊢ (𝐾 ∈ N → ([⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R +R 1R) = [⟨((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) +P (1P +P 1P)), (1P +P 1P)⟩] ~R )
29		addpinq1 7077	. . . . . . . . . . 11 ⊢ (𝐾 ∈ N → [⟨(𝐾 +N 1o), 1o⟩] ~Q = ([⟨𝐾, 1o⟩] ~Q +Q 1Q))
30	29	breq2d 3863	. . . . . . . . . 10 ⊢ (𝐾 ∈ N → (𝑙 <Q [⟨(𝐾 +N 1o), 1o⟩] ~Q ↔ 𝑙 <Q ([⟨𝐾, 1o⟩] ~Q +Q 1Q)))
31	30	abbidv 2206	. . . . . . . . 9 ⊢ (𝐾 ∈ N → {𝑙 ∣ 𝑙 <Q [⟨(𝐾 +N 1o), 1o⟩] ~Q } = {𝑙 ∣ 𝑙 <Q ([⟨𝐾, 1o⟩] ~Q +Q 1Q)})
32	29	breq1d 3861	. . . . . . . . . 10 ⊢ (𝐾 ∈ N → ([⟨(𝐾 +N 1o), 1o⟩] ~Q <Q 𝑢 ↔ ([⟨𝐾, 1o⟩] ~Q +Q 1Q) <Q 𝑢))
33	32	abbidv 2206	. . . . . . . . 9 ⊢ (𝐾 ∈ N → {𝑢 ∣ [⟨(𝐾 +N 1o), 1o⟩] ~Q <Q 𝑢} = {𝑢 ∣ ([⟨𝐾, 1o⟩] ~Q +Q 1Q) <Q 𝑢})
34	31, 33	opeq12d 3636	. . . . . . . 8 ⊢ (𝐾 ∈ N → ⟨{𝑙 ∣ 𝑙 <Q [⟨(𝐾 +N 1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝐾 +N 1o), 1o⟩] ~Q <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q ([⟨𝐾, 1o⟩] ~Q +Q 1Q)}, {𝑢 ∣ ([⟨𝐾, 1o⟩] ~Q +Q 1Q) <Q 𝑢}⟩)
35		nnnq 7035	. . . . . . . . 9 ⊢ (𝐾 ∈ N → [⟨𝐾, 1o⟩] ~Q ∈ Q)
36		addnqpr1 7175	. . . . . . . . 9 ⊢ ([⟨𝐾, 1o⟩] ~Q ∈ Q → ⟨{𝑙 ∣ 𝑙 <Q ([⟨𝐾, 1o⟩] ~Q +Q 1Q)}, {𝑢 ∣ ([⟨𝐾, 1o⟩] ~Q +Q 1Q) <Q 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P))
37	35, 36	syl 14	. . . . . . . 8 ⊢ (𝐾 ∈ N → ⟨{𝑙 ∣ 𝑙 <Q ([⟨𝐾, 1o⟩] ~Q +Q 1Q)}, {𝑢 ∣ ([⟨𝐾, 1o⟩] ~Q +Q 1Q) <Q 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P))
38	34, 37	eqtrd 2121	. . . . . . 7 ⊢ (𝐾 ∈ N → ⟨{𝑙 ∣ 𝑙 <Q [⟨(𝐾 +N 1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝐾 +N 1o), 1o⟩] ~Q <Q 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P))
39	38	oveq1d 5681	. . . . . 6 ⊢ (𝐾 ∈ N → (⟨{𝑙 ∣ 𝑙 <Q [⟨(𝐾 +N 1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝐾 +N 1o), 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) = ((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) +P 1P))
40	39	opeq1d 3634	. . . . 5 ⊢ (𝐾 ∈ N → ⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨(𝐾 +N 1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝐾 +N 1o), 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩ = ⟨((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) +P 1P), 1P⟩)
41	40	eceq1d 6342	. . . 4 ⊢ (𝐾 ∈ N → [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨(𝐾 +N 1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝐾 +N 1o), 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R = [⟨((⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P) +P 1P), 1P⟩] ~R )
42	19, 28, 41	3eqtr4d 2131	. . 3 ⊢ (𝐾 ∈ N → ([⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R +R 1R) = [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨(𝐾 +N 1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝐾 +N 1o), 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
43	42	opeq1d 3634	. 2 ⊢ (𝐾 ∈ N → ⟨([⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R +R 1R), 0R⟩ = ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨(𝐾 +N 1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝐾 +N 1o), 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
44	17, 43	eqtrd 2121	1 ⊢ (𝐾 ∈ N → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ + 1) = ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨(𝐾 +N 1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝐾 +N 1o), 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1290   ∈ wcel 1439  {cab 2075  ⟨cop 3453   class class class wbr 3851   × cxp 4449  (class class class)co 5666  1_oc1o 6188  [cec 6304   / cqs 6305  Ncnpi 6885   +_N cpli 6886   ~_Q ceq 6892  Qcnq 6893  1_Qc1q 6894   +_Q cplq 6895   <_Q cltq 6898  Pcnp 6904  1_Pc1p 6905   +_P cpp 6906   ~_R cer 6909  Rcnr 6910  0_Rc0r 6911  1_Rc1r 6912   +_R cplr 6914  1c1 7405   + caddc 7407

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-coll 3960  ax-sep 3963  ax-nul 3971  ax-pow 4015  ax-pr 4045  ax-un 4269  ax-setind 4366  ax-iinf 4416

This theorem depends on definitions:  df-bi 116  df-dc 782  df-3or 926  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-reu 2367  df-rab 2369  df-v 2622  df-sbc 2842  df-csb 2935  df-dif 3002  df-un 3004  df-in 3006  df-ss 3013  df-nul 3288  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-int 3695  df-iun 3738  df-br 3852  df-opab 3906  df-mpt 3907  df-tr 3943  df-eprel 4125  df-id 4129  df-po 4132  df-iso 4133  df-iord 4202  df-on 4204  df-suc 4207  df-iom 4419  df-xp 4457  df-rel 4458  df-cnv 4459  df-co 4460  df-dm 4461  df-rn 4462  df-res 4463  df-ima 4464  df-iota 4993  df-fun 5030  df-fn 5031  df-f 5032  df-f1 5033  df-fo 5034  df-f1o 5035  df-fv 5036  df-ov 5669  df-oprab 5670  df-mpt2 5671  df-1st 5925  df-2nd 5926  df-recs 6084  df-irdg 6149  df-1o 6195  df-2o 6196  df-oadd 6199  df-omul 6200  df-er 6306  df-ec 6308  df-qs 6312  df-ni 6917  df-pli 6918  df-mi 6919  df-lti 6920  df-plpq 6957  df-mpq 6958  df-enq 6960  df-nqqs 6961  df-plqqs 6962  df-mqqs 6963  df-1nqqs 6964  df-rq 6965  df-ltnqqs 6966  df-enq0 7037  df-nq0 7038  df-0nq0 7039  df-plq0 7040  df-mq0 7041  df-inp 7079  df-i1p 7080  df-iplp 7081  df-enr 7326  df-nr 7327  df-plr 7328  df-0r 7331  df-1r 7332  df-c 7410  df-1 7412  df-add 7415

This theorem is referenced by:  pitonn  7439  nntopi  7483