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 14794

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 14793	. 2 ⊢ 𝑆:ℕ_∞⟶ℕ_∞
3		fveq1 5516	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑥 → (𝑓‘suc 𝑗) = (𝑥‘suc 𝑗))
4		fveq1 5516	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑥 → (𝑓‘𝑗) = (𝑥‘𝑗))
5	3, 4	sseq12d 3188	. . . . . . . . . 10 ⊢ (𝑓 = 𝑥 → ((𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ (𝑥‘suc 𝑗) ⊆ (𝑥‘𝑗)))
6	5	ralbidv 2477	. . . . . . . . 9 ⊢ (𝑓 = 𝑥 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ∀𝑗 ∈ ω (𝑥‘suc 𝑗) ⊆ (𝑥‘𝑗)))
7		df-nninf 7121	. . . . . . . . 9 ⊢ ℕ_∞ = {𝑓 ∈ (2_o ↑_𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗)}
8	6, 7	elrab2 2898	. . . . . . . 8 ⊢ (𝑥 ∈ ℕ_∞ ↔ (𝑥 ∈ (2_o ↑_𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑥‘suc 𝑗) ⊆ (𝑥‘𝑗)))
9	8	simplbi 274	. . . . . . 7 ⊢ (𝑥 ∈ ℕ_∞ → 𝑥 ∈ (2_o ↑_𝑚 ω))
10		elmapfn 6673	. . . . . . 7 ⊢ (𝑥 ∈ (2_o ↑_𝑚 ω) → 𝑥 Fn ω)
11	9, 10	syl 14	. . . . . 6 ⊢ (𝑥 ∈ ℕ_∞ → 𝑥 Fn ω)
12	11	ad2antrr 488	. . . . 5 ⊢ (((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) → 𝑥 Fn ω)
13		fveq1 5516	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑦 → (𝑓‘suc 𝑗) = (𝑦‘suc 𝑗))
14		fveq1 5516	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑦 → (𝑓‘𝑗) = (𝑦‘𝑗))
15	13, 14	sseq12d 3188	. . . . . . . . . 10 ⊢ (𝑓 = 𝑦 → ((𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ (𝑦‘suc 𝑗) ⊆ (𝑦‘𝑗)))
16	15	ralbidv 2477	. . . . . . . . 9 ⊢ (𝑓 = 𝑦 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ∀𝑗 ∈ ω (𝑦‘suc 𝑗) ⊆ (𝑦‘𝑗)))
17	16, 7	elrab2 2898	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ_∞ ↔ (𝑦 ∈ (2_o ↑_𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑦‘suc 𝑗) ⊆ (𝑦‘𝑗)))
18	17	simplbi 274	. . . . . . 7 ⊢ (𝑦 ∈ ℕ_∞ → 𝑦 ∈ (2_o ↑_𝑚 ω))
19		elmapfn 6673	. . . . . . 7 ⊢ (𝑦 ∈ (2_o ↑_𝑚 ω) → 𝑦 Fn ω)
20	18, 19	syl 14	. . . . . 6 ⊢ (𝑦 ∈ ℕ_∞ → 𝑦 Fn ω)
21	20	ad2antlr 489	. . . . 5 ⊢ (((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) → 𝑦 Fn ω)
22		simplr 528	. . . . . . 7 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → (𝑆‘𝑥) = (𝑆‘𝑦))
23	22	fveq1d 5519	. . . . . 6 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆‘𝑥)‘suc 𝑘) = ((𝑆‘𝑦)‘suc 𝑘))
24		fveq1 5516	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑥 → (𝑝‘∪ 𝑖) = (𝑥‘∪ 𝑖))
25	24	ifeq2d 3554	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑥 → if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖)) = if(𝑖 = ∅, 1_o, (𝑥‘∪ 𝑖)))
26	25	mpteq2dv 4096	. . . . . . . . . 10 ⊢ (𝑝 = 𝑥 → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖))) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑥‘∪ 𝑖))))
27		omex 4594	. . . . . . . . . . 11 ⊢ ω ∈ V
28	27	mptex 5744	. . . . . . . . . 10 ⊢ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑥‘∪ 𝑖))) ∈ V
29	26, 1, 28	fvmpt 5595	. . . . . . . . 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 3822	. . . . . . . . . 10 ⊢ (((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → ∪ 𝑖 = ∪ suc 𝑘)
34	33	fveq2d 5521	. . . . . . . . 9 ⊢ (((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → (𝑥‘∪ 𝑖) = (𝑥‘∪ suc 𝑘))
35	32, 34	ifbieq2d 3560	. . . . . . . 8 ⊢ (((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → if(𝑖 = ∅, 1_o, (𝑥‘∪ 𝑖)) = if(suc 𝑘 = ∅, 1_o, (𝑥‘∪ suc 𝑘)))
36		peano2 4596	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
37	36	adantl 277	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ ω)
38		1lt2o 6445	. . . . . . . . . 10 ⊢ 1_o ∈ 2_o
39	38	a1i 9	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → 1_o ∈ 2_o)
40		nninff 7123	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℕ_∞ → 𝑥:ω⟶2_o)
41	40	ad3antrrr 492	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → 𝑥:ω⟶2_o)
42		nnpredcl 4624	. . . . . . . . . . 11 ⊢ (suc 𝑘 ∈ ω → ∪ suc 𝑘 ∈ ω)
43	37, 42	syl 14	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → ∪ suc 𝑘 ∈ ω)
44	41, 43	ffvelcdmd 5654	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → (𝑥‘∪ suc 𝑘) ∈ 2_o)
45		nndceq0 4619	. . . . . . . . . 10 ⊢ (suc 𝑘 ∈ ω → DECID suc 𝑘 = ∅)
46	37, 45	syl 14	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → DECID suc 𝑘 = ∅)
47	39, 44, 46	ifcldcd 3572	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → if(suc 𝑘 = ∅, 1_o, (𝑥‘∪ suc 𝑘)) ∈ 2_o)
48	30, 35, 37, 47	fvmptd 5599	. . . . . . 7 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆‘𝑥)‘suc 𝑘) = if(suc 𝑘 = ∅, 1_o, (𝑥‘∪ suc 𝑘)))
49		peano3 4597	. . . . . . . . . 10 ⊢ (𝑘 ∈ ω → suc 𝑘 ≠ ∅)
50	49	adantl 277	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → suc 𝑘 ≠ ∅)
51	50	neneqd 2368	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → ¬ suc 𝑘 = ∅)
52	51	iffalsed 3546	. . . . . . 7 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → if(suc 𝑘 = ∅, 1_o, (𝑥‘∪ suc 𝑘)) = (𝑥‘∪ suc 𝑘))
53		nnord 4613	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ω → Ord 𝑘)
54		ordtr 4380	. . . . . . . . . . 11 ⊢ (Ord 𝑘 → Tr 𝑘)
55	53, 54	syl 14	. . . . . . . . . 10 ⊢ (𝑘 ∈ ω → Tr 𝑘)
56		unisucg 4416	. . . . . . . . . 10 ⊢ (𝑘 ∈ ω → (Tr 𝑘 ↔ ∪ suc 𝑘 = 𝑘))
57	55, 56	mpbid 147	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → ∪ suc 𝑘 = 𝑘)
58	57	fveq2d 5521	. . . . . . . 8 ⊢ (𝑘 ∈ ω → (𝑥‘∪ suc 𝑘) = (𝑥‘𝑘))
59	58	adantl 277	. . . . . . 7 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → (𝑥‘∪ suc 𝑘) = (𝑥‘𝑘))
60	48, 52, 59	3eqtrd 2214	. . . . . 6 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆‘𝑥)‘suc 𝑘) = (𝑥‘𝑘))
61		fveq1 5516	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑦 → (𝑝‘∪ 𝑖) = (𝑦‘∪ 𝑖))
62	61	ifeq2d 3554	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑦 → if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖)) = if(𝑖 = ∅, 1_o, (𝑦‘∪ 𝑖)))
63	62	mpteq2dv 4096	. . . . . . . . . 10 ⊢ (𝑝 = 𝑦 → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖))) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑦‘∪ 𝑖))))
64	27	mptex 5744	. . . . . . . . . 10 ⊢ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑦‘∪ 𝑖))) ∈ V
65	63, 1, 64	fvmpt 5595	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ_∞ → (𝑆‘𝑦) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑦‘∪ 𝑖))))
66	65	ad3antlr 493	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → (𝑆‘𝑦) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑦‘∪ 𝑖))))
67	33	fveq2d 5521	. . . . . . . . 9 ⊢ (((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → (𝑦‘∪ 𝑖) = (𝑦‘∪ suc 𝑘))
68	32, 67	ifbieq2d 3560	. . . . . . . 8 ⊢ (((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → if(𝑖 = ∅, 1_o, (𝑦‘∪ 𝑖)) = if(suc 𝑘 = ∅, 1_o, (𝑦‘∪ suc 𝑘)))
69		nninff 7123	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ_∞ → 𝑦:ω⟶2_o)
70	69	ad3antlr 493	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → 𝑦:ω⟶2_o)
71	70, 43	ffvelcdmd 5654	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → (𝑦‘∪ suc 𝑘) ∈ 2_o)
72	39, 71, 46	ifcldcd 3572	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → if(suc 𝑘 = ∅, 1_o, (𝑦‘∪ suc 𝑘)) ∈ 2_o)
73	66, 68, 37, 72	fvmptd 5599	. . . . . . 7 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆‘𝑦)‘suc 𝑘) = if(suc 𝑘 = ∅, 1_o, (𝑦‘∪ suc 𝑘)))
74	51	iffalsed 3546	. . . . . . 7 ⊢ ((((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) ∧ 𝑘 ∈ ω) → if(suc 𝑘 = ∅, 1_o, (𝑦‘∪ suc 𝑘)) = (𝑦‘∪ suc 𝑘))
75	57	fveq2d 5521	. . . . . . . 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 5618	. . . 4 ⊢ (((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) ∧ (𝑆‘𝑥) = (𝑆‘𝑦)) → 𝑥 = 𝑦)
80	79	ex 115	. . 3 ⊢ ((𝑥 ∈ ℕ_∞ ∧ 𝑦 ∈ ℕ_∞) → ((𝑆‘𝑥) = (𝑆‘𝑦) → 𝑥 = 𝑦))
81	80	rgen2a 2531	. 2 ⊢ ∀𝑥 ∈ ℕ_∞ ∀𝑦 ∈ ℕ_∞ ((𝑆‘𝑥) = (𝑆‘𝑦) → 𝑥 = 𝑦)
82		dff13 5771	. 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 3131 ∅c0 3424 ifcif 3536 ∪ cuni 3811 ↦ cmpt 4066 Tr wtr 4103 Ord word 4364 suc csuc 4367 ωcom 4591 Fn wfn 5213 ⟶wf 5214 –1-1→wf1 5215 ‘cfv 5218 (class class class)co 5877 1_oc1o 6412 2_oc2o 6413 ↑_𝑚 cmap 6650 ℕ_∞xnninf 7120

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 4120 ax-sep 4123 ax-nul 4131 ax-pow 4176 ax-pr 4211 ax-un 4435 ax-setind 4538 ax-iinf 4589

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 2741 df-sbc 2965 df-csb 3060 df-dif 3133 df-un 3135 df-in 3137 df-ss 3144 df-nul 3425 df-if 3537 df-pw 3579 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-int 3847 df-iun 3890 df-br 4006 df-opab 4067 df-mpt 4068 df-tr 4104 df-id 4295 df-iord 4368 df-on 4370 df-suc 4373 df-iom 4592 df-xp 4634 df-rel 4635 df-cnv 4636 df-co 4637 df-dm 4638 df-rn 4639 df-res 4640 df-ima 4641 df-iota 5180 df-fun 5220 df-fn 5221 df-f 5222 df-f1 5223 df-fo 5224 df-f1o 5225 df-fv 5226 df-ov 5880 df-oprab 5881 df-mpo 5882 df-1o 6419 df-2o 6420 df-map 6652 df-nninf 7121

This theorem is referenced by: exmidsbthrlem 14809

W3C validator