infensuc

Description: Any infinite ordinal is equinumerous to its successor. Exercise 7 of TakeutiZaring p. 88. Proved without the Axiom of Infinity. (Contributed by NM, 30-Oct-2003) (Revised by Mario Carneiro, 13-Jan-2013)

		Ref	Expression
	Assertion	infensuc	$⊢ (A \in On \land ω \subseteq A) \to A \approx suc A$

Proof

Step	Hyp	Ref	Expression
1		onprc	$⊢ \neg On \in V$
2		eleq1	$⊢ ω = On \to (ω \in V \leftrightarrow On \in V)$
3	1 2	mtbiri	$⊢ ω = On \to \neg ω \in V$
4		ssexg	$⊢ (ω \subseteq A \land A \in On) \to ω \in V$
5	4	ancoms	$⊢ (A \in On \land ω \subseteq A) \to ω \in V$
6	3 5	nsyl3	$⊢ (A \in On \land ω \subseteq A) \to \neg ω = On$
7		omon	$⊢ (ω \in On \lor ω = On)$
8	7	ori	$⊢ \neg ω \in On \to ω = On$
9	6 8	nsyl2	$⊢ (A \in On \land ω \subseteq A) \to ω \in On$
10		id	$⊢ x = ω \to x = ω$
11		suceq	$⊢ x = ω \to suc x = suc ω$
12	10 11	breq12d	$⊢ x = ω \to (x \approx suc x \leftrightarrow ω \approx suc ω)$
13		id	$⊢ x = y \to x = y$
14		suceq	$⊢ x = y \to suc x = suc y$
15	13 14	breq12d	$⊢ x = y \to (x \approx suc x \leftrightarrow y \approx suc y)$
16		id	$⊢ x = suc y \to x = suc y$
17		suceq	$⊢ x = suc y \to suc x = suc suc y$
18	16 17	breq12d	$⊢ x = suc y \to (x \approx suc x \leftrightarrow suc y \approx suc suc y)$
19		id	$⊢ x = A \to x = A$
20		suceq	$⊢ x = A \to suc x = suc A$
21	19 20	breq12d	$⊢ x = A \to (x \approx suc x \leftrightarrow A \approx suc A)$
22		limom	$⊢ Lim ω$
23	22	limensuci	$⊢ ω \in On \to ω \approx suc ω$
24		vex	$⊢ y \in V$
25	24	sucex	$⊢ suc y \in V$
26		en2sn	$⊢ (y \in V \land suc y \in V) \to \{y\} \approx \{suc y\}$
27	24 25 26	mp2an	$⊢ \{y\} \approx \{suc y\}$
28		eloni	$⊢ y \in On \to Ord y$
29		ordirr	$⊢ Ord y \to \neg y \in y$
30	28 29	syl	$⊢ y \in On \to \neg y \in y$
31		disjsn	$⊢ y \cap \{y\} = \emptyset \leftrightarrow \neg y \in y$
32	30 31	sylibr	$⊢ y \in On \to y \cap \{y\} = \emptyset$
33		eloni	$⊢ suc y \in On \to Ord suc y$
34		ordirr	$⊢ Ord suc y \to \neg suc y \in suc y$
35	33 34	syl	$⊢ suc y \in On \to \neg suc y \in suc y$
36		sucelon	$⊢ y \in On \leftrightarrow suc y \in On$
37		disjsn	$⊢ suc y \cap \{suc y\} = \emptyset \leftrightarrow \neg suc y \in suc y$
38	35 36 37	3imtr4i	$⊢ y \in On \to suc y \cap \{suc y\} = \emptyset$
39	32 38	jca	$⊢ y \in On \to (y \cap \{y\} = \emptyset \land suc y \cap \{suc y\} = \emptyset)$
40		unen	$⊢ ((y \approx suc y \land \{y\} \approx \{suc y\}) \land (y \cap \{y\} = \emptyset \land suc y \cap \{suc y\} = \emptyset)) \to (y \cup \{y\}) \approx (suc y \cup \{suc y\})$
41		df-suc	$⊢ suc y = y \cup \{y\}$
42		df-suc	$⊢ suc suc y = suc y \cup \{suc y\}$
43	40 41 42	3brtr4g	$⊢ ((y \approx suc y \land \{y\} \approx \{suc y\}) \land (y \cap \{y\} = \emptyset \land suc y \cap \{suc y\} = \emptyset)) \to suc y \approx suc suc y$
44	43	ex	$⊢ (y \approx suc y \land \{y\} \approx \{suc y\}) \to ((y \cap \{y\} = \emptyset \land suc y \cap \{suc y\} = \emptyset) \to suc y \approx suc suc y)$
45	39 44	syl5	$⊢ (y \approx suc y \land \{y\} \approx \{suc y\}) \to (y \in On \to suc y \approx suc suc y)$
46	27 45	mpan2	$⊢ y \approx suc y \to (y \in On \to suc y \approx suc suc y)$
47	46	com12	$⊢ y \in On \to (y \approx suc y \to suc y \approx suc suc y)$
48	47	ad2antrr	$⊢ ((y \in On \land ω \in On) \land ω \subseteq y) \to (y \approx suc y \to suc y \approx suc suc y)$
49		vex	$⊢ x \in V$
50		limensuc	$⊢ (x \in V \land Lim x) \to x \approx suc x$
51	49 50	mpan	$⊢ Lim x \to x \approx suc x$
52	51	ad2antrr	$⊢ ((Lim x \land ω \in On) \land ω \subseteq x) \to x \approx suc x$
53	52	a1d	$⊢ ((Lim x \land ω \in On) \land ω \subseteq x) \to (\forall y \in x (ω \subseteq y \to y \approx suc y) \to x \approx suc x)$
54	12 15 18 21 23 48 53	tfindsg	$⊢ ((A \in On \land ω \in On) \land ω \subseteq A) \to A \approx suc A$
55	54	exp31	$⊢ A \in On \to (ω \in On \to (ω \subseteq A \to A \approx suc A))$
56	55	com23	$⊢ A \in On \to (ω \subseteq A \to (ω \in On \to A \approx suc A))$
57	56	imp	$⊢ (A \in On \land ω \subseteq A) \to (ω \in On \to A \approx suc A)$
58	9 57	mpd	$⊢ (A \in On \land ω \subseteq A) \to A \approx suc A$

Metamath Proof Explorer

Theorem infensuc

Proof