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 iota. (Contributed by Mario Carneiro, 10-Oct-2014.)

Assertion

Ref	Expression
ax-inf	|- T. |= (E.\f:(iota -> iota) [(1-1 f:(iota -> iota)) /\ (~ (onto f:(iota -> iota)))])

Detailed syntax breakdown of Axiom ax-inf

Step	Hyp	Ref	Expression
1		kt 8	. 2 term T.
2		tex 123	. . 3 term E.
3		hi 4	. . . . 5 type iota
4	3, 3	ht 2	. . . 4 type (iota -> iota)
5		vf	. . . 4 var f
6		tf11 189	. . . . . 6 term 1-1
7	4, 5	tv 1	. . . . . 6 term f:(iota -> iota)
8	6, 7	kc 5	. . . . 5 term (1-1 f:(iota -> iota))
9		tne 120	. . . . . 6 term ~
10		tfo 190	. . . . . . 7 term onto
11	10, 7	kc 5	. . . . . 6 term (onto f:(iota -> iota))
12	9, 11	kc 5	. . . . 5 term (~ (onto f:(iota -> iota)))
13		tan 119	. . . . 5 term /\
14	8, 12, 13	kbr 9	. . . 4 term [(1-1 f:(iota -> iota)) /\ (~ (onto f:(iota -> iota)))]
15	4, 5, 14	kl 6	. . 3 term \f:(iota -> iota) [(1-1 f:(iota -> iota)) /\ (~ (onto f:(iota -> iota)))]
16	2, 15	kc 5	. 2 term (E.\f:(iota -> iota) [(1-1 f:(iota -> iota)) /\ (~ (onto f:(iota -> iota)))])
17	1, 16	wffMMJ2 11	1 wff T. |= (E.\f:(iota -> iota) [(1-1 f:(iota -> iota)) /\ (~ (onto f:(iota -> iota)))])

This axiom is referenced by: (None)