Axiom ax-inf 202

Description: The axiom of infinity: the set of "individuals" is not Dedekind-finite. Using the axiom of choice, we can show that this is equivalent to an embedding of the natural numbers in ι. (Contributed by Mario Carneiro, 10-Oct-2014.)

Assertion

Ref	Expression
ax-inf	⊢ ⊤⊧(∃λf:(ι → ι) [(1-1 f:(ι → ι)) ∧ (¬ (onto f:(ι → ι)))])

Detailed syntax breakdown of Axiom ax-inf

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		tex 123	. . 3 term ∃
3		hi 4	. . . . 5 type ι
4	3, 3	ht 2	. . . 4 type (ι → ι)
5		vf	. . . 4 var f
6		tf11 189	. . . . . 6 term 1-1
7	4, 5	tv 1	. . . . . 6 term f:(ι → ι)
8	6, 7	kc 5	. . . . 5 term (1-1 f:(ι → ι))
9		tne 120	. . . . . 6 term ¬
10		tfo 190	. . . . . . 7 term onto
11	10, 7	kc 5	. . . . . 6 term (onto f:(ι → ι))
12	9, 11	kc 5	. . . . 5 term (¬ (onto f:(ι → ι)))
13		tan 119	. . . . 5 term ∧
14	8, 12, 13	kbr 9	. . . 4 term [(1-1 f:(ι → ι)) ∧ (¬ (onto f:(ι → ι)))]
15	4, 5, 14	kl 6	. . 3 term λf:(ι → ι) [(1-1 f:(ι → ι)) ∧ (¬ (onto f:(ι → ι)))]
16	2, 15	kc 5	. 2 term (∃λf:(ι → ι) [(1-1 f:(ι → ι)) ∧ (¬ (onto f:(ι → ι)))])
17	1, 16	wffMMJ2 11	1 wff ⊤⊧(∃λf:(ι → ι) [(1-1 f:(ι → ι)) ∧ (¬ (onto f:(ι → ι)))])

This axiom is used by: (None)