peano4nninf - Mathbox for Jim Kingdon

	Mathbox for Jim Kingdon		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > Mathboxes > peano4nninf		GIF version

Theorem peano4nninf 14725

Description: The successor function on ℕ_∞ is one to one. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 31-Jul-2022.)

**Hypothesis**
Ref	Expression
peano4nninf.s	⊢ 𝑆 = (𝑝 ∈ ℕ_∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖))))

**Assertion**
Ref	Expression
peano4nninf	⊢ 𝑆:ℕ_∞–1-1→ℕ_∞

Distinct variable groups: 𝑆,𝑖 𝑖,𝑝 Allowed substitution hint: 𝑆(𝑝)

Proof of Theorem peano4nninf Dummy variables 𝑘 𝑥 𝑦 𝑓 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		peano4nninf.s	. . 3 ⊢ 𝑆 = (𝑝 ∈ ℕ_∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖))))
2	1	nnsf 14724	. 2 ⊢ 𝑆:ℕ_∞⟶ℕ_∞
3		fveq1 5514	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑥 → (𝑓‘suc 𝑗) = (𝑥‘suc 𝑗))
4		fveq1 5514	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑥 → (𝑓‘𝑗) = (𝑥‘𝑗))
5	3, 4	sseq12d 3186	. . . . . . . . . 10 ⊢ (𝑓 = 𝑥 → ((𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ (𝑥‘suc 𝑗) ⊆ (𝑥‘𝑗)))
6	5	ralbidv 2477	. . . . . . . . 9 ⊢ (𝑓 = 𝑥 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ∀𝑗 ∈ ω (𝑥‘suc 𝑗) ⊆ (𝑥‘𝑗)))
7		df-nninf 7118	. . . . . . . . 9 ⊢ ℕ_∞ = {𝑓 ∈ (2_o ↑_𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗)}
8	6, 7	elrab2 2896	. . . . . . . 8 ⊢ (𝑥 ∈ ℕ_∞ ↔ (𝑥 ∈ (2_o ↑_𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑥‘suc 𝑗) ⊆ (𝑥‘𝑗)))
9	8	simplbi 274	. . . . . . 7 ⊢ (𝑥 ∈ ℕ_∞ → 𝑥 ∈ (2_o ↑_𝑚 ω))
10		elmapfn 6670	. . . . . . 7 ⊢ (𝑥 ∈ (2_o ↑_𝑚 ω) → 𝑥 Fn ω)
11	9, 10	syl 14	. . . . . 6 ⊢ (𝑥 ∈ ℕ_∞ → 𝑥 Fn ω)
12	11	ad2antrr 488	. . . . 5 ⊢ (((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) → 𝑥 Fn ω)
13		fveq1 5514	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑦 → (𝑓‘suc 𝑗) = (𝑦‘suc 𝑗))
14		fveq1 5514	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑦 → (𝑓‘𝑗) = (𝑦‘𝑗))
15	13, 14	sseq12d 3186	. . . . . . . . . 10 ⊢ (𝑓 = 𝑦 → ((𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ (𝑦‘suc 𝑗) ⊆ (𝑦‘𝑗)))
16	15	ralbidv 2477	. . . . . . . . 9 ⊢ (𝑓 = 𝑦 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ∀𝑗 ∈ ω (𝑦‘suc 𝑗) ⊆ (𝑦‘𝑗)))
17	16, 7	elrab2 2896	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ_∞ ↔ (𝑦 ∈ (2_o ↑_𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑦‘suc 𝑗) ⊆ (𝑦‘𝑗)))
18	17	simplbi 274	. . . . . . 7 ⊢ (𝑦 ∈ ℕ_∞ → 𝑦 ∈ (2_o ↑_𝑚 ω))
19		elmapfn 6670	. . . . . . 7 ⊢ (𝑦 ∈ (2_o ↑_𝑚 ω) → 𝑦 Fn ω)
20	18, 19	syl 14	. . . . . 6 ⊢ (𝑦 ∈ ℕ_∞ → 𝑦 Fn ω)
21	20	ad2antlr 489	. . . . 5 ⊢ (((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) → 𝑦 Fn ω)
22		simplr 528	. . . . . . 7 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → (𝑆‘𝑥) = (𝑆‘𝑦))
23	22	fveq1d 5517	. . . . . 6 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆‘𝑥)‘suc 𝑘) = ((𝑆‘𝑦)‘suc 𝑘))
24		fveq1 5514	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑥 → (𝑝‘∪ 𝑖) = (𝑥‘∪ 𝑖))
25	24	ifeq2d 3552	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑥 → if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖)) = if(𝑖 = ∅, 1_o, (𝑥‘∪ 𝑖)))
26	25	mpteq2dv 4094	. . . . . . . . . 10 ⊢ (𝑝 = 𝑥 → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖))) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑥‘∪ 𝑖))))
27		omex 4592	. . . . . . . . . . 11 ⊢ ω ∈ V
28	27	mptex 5742	. . . . . . . . . 10 ⊢ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑥‘∪ 𝑖))) ∈ V
29	26, 1, 28	fvmpt 5593	. . . . . . . . 9 ⊢ (𝑥 ∈ ℕ_∞ → (𝑆‘𝑥) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑥‘∪ 𝑖))))
30	29	ad3antrrr 492	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → (𝑆‘𝑥) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑥‘∪ 𝑖))))
31		simpr 110	. . . . . . . . . 10 ⊢ (((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → 𝑖 = suc 𝑘)
32	31	eqeq1d 2186	. . . . . . . . 9 ⊢ (((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → (𝑖 = ∅ ↔ suc 𝑘 = ∅))
33	31	unieqd 3820	. . . . . . . . . 10 ⊢ (((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → ∪ 𝑖 = ∪ suc 𝑘)
34	33	fveq2d 5519	. . . . . . . . 9 ⊢ (((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → (𝑥‘∪ 𝑖) = (𝑥‘∪ suc 𝑘))
35	32, 34	ifbieq2d 3558	. . . . . . . 8 ⊢ (((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → if(𝑖 = ∅, 1_o, (𝑥‘∪ 𝑖)) = if(suc 𝑘 = ∅, 1_o, (𝑥‘∪ suc 𝑘)))
36		peano2 4594	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
37	36	adantl 277	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ ω)
38		1lt2o 6442	. . . . . . . . . 10 ⊢ 1_o ∈ 2_o
39	38	a1i 9	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → 1_o ∈ 2_o)
40		nninff 7120	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℕ_∞ → 𝑥:ω⟶2_o)
41	40	ad3antrrr 492	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → 𝑥:ω⟶2_o)
42		nnpredcl 4622	. . . . . . . . . . 11 ⊢ (suc 𝑘 ∈ ω → ∪ suc 𝑘 ∈ ω)
43	37, 42	syl 14	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → ∪ suc 𝑘 ∈ ω)
44	41, 43	ffvelcdmd 5652	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → (𝑥‘∪ suc 𝑘) ∈ 2_o)
45		nndceq0 4617	. . . . . . . . . 10 ⊢ (suc 𝑘 ∈ ω → DECID suc 𝑘 = ∅)
46	37, 45	syl 14	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → DECID suc 𝑘 = ∅)
47	39, 44, 46	ifcldcd 3570	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → if(suc 𝑘 = ∅, 1_o, (𝑥‘∪ suc 𝑘)) ∈ 2_o)
48	30, 35, 37, 47	fvmptd 5597	. . . . . . 7 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆‘𝑥)‘suc 𝑘) = if(suc 𝑘 = ∅, 1_o, (𝑥‘∪ suc 𝑘)))
49		peano3 4595	. . . . . . . . . 10 ⊢ (𝑘 ∈ ω → suc 𝑘 ≠ ∅)
50	49	adantl 277	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → suc 𝑘 ≠ ∅)
51	50	neneqd 2368	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → ¬ suc 𝑘 = ∅)
52	51	iffalsed 3544	. . . . . . 7 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → if(suc 𝑘 = ∅, 1_o, (𝑥‘∪ suc 𝑘)) = (𝑥‘∪ suc 𝑘))
53		nnord 4611	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ω → Ord 𝑘)
54		ordtr 4378	. . . . . . . . . . 11 ⊢ (Ord 𝑘 → Tr 𝑘)
55	53, 54	syl 14	. . . . . . . . . 10 ⊢ (𝑘 ∈ ω → Tr 𝑘)
56		unisucg 4414	. . . . . . . . . 10 ⊢ (𝑘 ∈ ω → (Tr 𝑘 ↔ ∪ suc 𝑘 = 𝑘))
57	55, 56	mpbid 147	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → ∪ suc 𝑘 = 𝑘)
58	57	fveq2d 5519	. . . . . . . 8 ⊢ (𝑘 ∈ ω → (𝑥‘∪ suc 𝑘) = (𝑥‘𝑘))
59	58	adantl 277	. . . . . . 7 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → (𝑥‘∪ suc 𝑘) = (𝑥‘𝑘))
60	48, 52, 59	3eqtrd 2214	. . . . . 6 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆‘𝑥)‘suc 𝑘) = (𝑥‘𝑘))
61		fveq1 5514	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑦 → (𝑝‘∪ 𝑖) = (𝑦‘∪ 𝑖))
62	61	ifeq2d 3552	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑦 → if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖)) = if(𝑖 = ∅, 1_o, (𝑦‘∪ 𝑖)))
63	62	mpteq2dv 4094	. . . . . . . . . 10 ⊢ (𝑝 = 𝑦 → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖))) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑦‘∪ 𝑖))))
64	27	mptex 5742	. . . . . . . . . 10 ⊢ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑦‘∪ 𝑖))) ∈ V
65	63, 1, 64	fvmpt 5593	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ_∞ → (𝑆‘𝑦) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑦‘∪ 𝑖))))
66	65	ad3antlr 493	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → (𝑆‘𝑦) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑦‘∪ 𝑖))))
67	33	fveq2d 5519	. . . . . . . . 9 ⊢ (((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → (𝑦‘∪ 𝑖) = (𝑦‘∪ suc 𝑘))
68	32, 67	ifbieq2d 3558	. . . . . . . 8 ⊢ (((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → if(𝑖 = ∅, 1_o, (𝑦‘∪ 𝑖)) = if(suc 𝑘 = ∅, 1_o, (𝑦‘∪ suc 𝑘)))
69		nninff 7120	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ_∞ → 𝑦:ω⟶2_o)
70	69	ad3antlr 493	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → 𝑦:ω⟶2_o)
71	70, 43	ffvelcdmd 5652	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → (𝑦‘∪ suc 𝑘) ∈ 2_o)
72	39, 71, 46	ifcldcd 3570	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → if(suc 𝑘 = ∅, 1_o, (𝑦‘∪ suc 𝑘)) ∈ 2_o)
73	66, 68, 37, 72	fvmptd 5597	. . . . . . 7 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆‘𝑦)‘suc 𝑘) = if(suc 𝑘 = ∅, 1_o, (𝑦‘∪ suc 𝑘)))
74	51	iffalsed 3544	. . . . . . 7 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → if(suc 𝑘 = ∅, 1_o, (𝑦‘∪ suc 𝑘)) = (𝑦‘∪ suc 𝑘))
75	57	fveq2d 5519	. . . . . . . 8 ⊢ (𝑘 ∈ ω → (𝑦‘∪ suc 𝑘) = (𝑦‘𝑘))
76	75	adantl 277	. . . . . . 7 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → (𝑦‘∪ suc 𝑘) = (𝑦‘𝑘))
77	73, 74, 76	3eqtrd 2214	. . . . . 6 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆‘𝑦)‘suc 𝑘) = (𝑦‘𝑘))
78	23, 60, 77	3eqtr3d 2218	. . . . 5 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → (𝑥‘𝑘) = (𝑦‘𝑘))
79	12, 21, 78	eqfnfvd 5616	. . . 4 ⊢ (((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) → 𝑥 = 𝑦)
80	79	ex 115	. . 3 ⊢ ((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) → ((𝑆‘𝑥) = (𝑆‘𝑦) → 𝑥 = 𝑦))
81	80	rgen2a 2531	. 2 ⊢ ∀𝑥 ∈ ℕ_∞ ∀𝑦 ∈ ℕ_∞ ((𝑆‘𝑥) = (𝑆‘𝑦) → 𝑥 = 𝑦)
82		dff13 5768	. 2 ⊢ (𝑆:ℕ_∞–1-1→ℕ_∞ ↔ (𝑆:ℕ_∞⟶ℕ_∞ ∧ ∀𝑥 ∈ ℕ_∞ ∀𝑦 ∈ ℕ_∞ ((𝑆‘𝑥) = (𝑆‘𝑦) → 𝑥 = 𝑦)))
83	2, 81, 82	mpbir2an 942	1 ⊢ 𝑆:ℕ_∞–1-1→ℕ_∞

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 DECID wdc 834 = wceq 1353 ∈ wcel 2148 ≠ wne 2347 ∀wral 2455 ⊆ wss 3129 ∅c0 3422 ifcif 3534 ∪ cuni 3809 ↦ cmpt 4064 Tr wtr 4101 Ord word 4362 suc csuc 4365 ωcom 4589 Fn wfn 5211 ⟶wf 5212 –1-1→wf1 5213 ‘cfv 5216 (class class class)co 5874 1_oc1o 6409 2_oc2o 6410 ↑_𝑚 cmap 6647 ℕ_∞xnninf 7117

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4118 ax-sep 4121 ax-nul 4129 ax-pow 4174 ax-pr 4209 ax-un 4433 ax-setind 4536 ax-iinf 4587

This theorem depends on definitions: df-bi 117 df-dc 835 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-ral 2460 df-rex 2461 df-reu 2462 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-if 3535 df-pw 3577 df-sn 3598 df-pr 3599 df-op 3601 df-uni 3810 df-int 3845 df-iun 3888 df-br 4004 df-opab 4065 df-mpt 4066 df-tr 4102 df-id 4293 df-iord 4366 df-on 4368 df-suc 4371 df-iom 4590 df-xp 4632 df-rel 4633 df-cnv 4634 df-co 4635 df-dm 4636 df-rn 4637 df-res 4638 df-ima 4639 df-iota 5178 df-fun 5218 df-fn 5219 df-f 5220 df-f1 5221 df-fo 5222 df-f1o 5223 df-fv 5224 df-ov 5877 df-oprab 5878 df-mpo 5879 df-1o 6416 df-2o 6417 df-map 6649 df-nninf 7118

This theorem is referenced by: exmidsbthrlem 14740

W3C validator