tfi

Description: The Principle of Transfinite Induction. Theorem 7.17 of TakeutiZaring p. 39. This principle states that if A is a class of ordinal numbers with the property that every ordinal number included in A also belongs to A , then every ordinal number is in A .

See Theorem tfindes or tfinds for the version involving basis and induction hypotheses. (Contributed by NM, 18-Feb-2004)

		Ref	Expression
	Assertion	tfi	$⊢ (A \subseteq On \land \forall x \in On (x \subseteq A \to x \in A)) \to A = On$

Proof

Step	Hyp	Ref	Expression
1		eldifn	$⊢ x \in (On ∖ A) \to \neg x \in A$
2	1	adantl	$⊢ ((x \in On \to (x \subseteq A \to x \in A)) \land x \in (On ∖ A)) \to \neg x \in A$
3		onss	$⊢ x \in On \to x \subseteq On$
4		difin0ss	$⊢ (On ∖ A) \cap x = \emptyset \to (x \subseteq On \to x \subseteq A)$
5	3 4	syl5com	$⊢ x \in On \to ((On ∖ A) \cap x = \emptyset \to x \subseteq A)$
6	5	imim1d	$⊢ x \in On \to ((x \subseteq A \to x \in A) \to ((On ∖ A) \cap x = \emptyset \to x \in A))$
7	6	a2i	$⊢ (x \in On \to (x \subseteq A \to x \in A)) \to (x \in On \to ((On ∖ A) \cap x = \emptyset \to x \in A))$
8		eldifi	$⊢ x \in (On ∖ A) \to x \in On$
9	7 8	impel	$⊢ ((x \in On \to (x \subseteq A \to x \in A)) \land x \in (On ∖ A)) \to ((On ∖ A) \cap x = \emptyset \to x \in A)$
10	2 9	mtod	$⊢ ((x \in On \to (x \subseteq A \to x \in A)) \land x \in (On ∖ A)) \to \neg (On ∖ A) \cap x = \emptyset$
11	10	ex	$⊢ (x \in On \to (x \subseteq A \to x \in A)) \to (x \in (On ∖ A) \to \neg (On ∖ A) \cap x = \emptyset)$
12	11	ralimi2	$⊢ \forall x \in On (x \subseteq A \to x \in A) \to \forall x \in (On ∖ A) \neg (On ∖ A) \cap x = \emptyset$
13		ralnex	$⊢ \forall x \in (On ∖ A) \neg (On ∖ A) \cap x = \emptyset \leftrightarrow \neg \exists x \in (On ∖ A) (On ∖ A) \cap x = \emptyset$
14	12 13	sylib	$⊢ \forall x \in On (x \subseteq A \to x \in A) \to \neg \exists x \in (On ∖ A) (On ∖ A) \cap x = \emptyset$
15		ssdif0	$⊢ On \subseteq A \leftrightarrow On ∖ A = \emptyset$
16	15	necon3bbii	$⊢ \neg On \subseteq A \leftrightarrow On ∖ A \neq \emptyset$
17		ordon	$⊢ Ord On$
18		difss	$⊢ On ∖ A \subseteq On$
19		tz7.5	$⊢ (Ord On \land On ∖ A \subseteq On \land On ∖ A \neq \emptyset) \to \exists x \in (On ∖ A) (On ∖ A) \cap x = \emptyset$
20	17 18 19	mp3an12	$⊢ On ∖ A \neq \emptyset \to \exists x \in (On ∖ A) (On ∖ A) \cap x = \emptyset$
21	16 20	sylbi	$⊢ \neg On \subseteq A \to \exists x \in (On ∖ A) (On ∖ A) \cap x = \emptyset$
22	14 21	nsyl2	$⊢ \forall x \in On (x \subseteq A \to x \in A) \to On \subseteq A$
23	22	anim2i	$⊢ (A \subseteq On \land \forall x \in On (x \subseteq A \to x \in A)) \to (A \subseteq On \land On \subseteq A)$
24		eqss	$⊢ A = On \leftrightarrow (A \subseteq On \land On \subseteq A)$
25	23 24	sylibr	$⊢ (A \subseteq On \land \forall x \in On (x \subseteq A \to x \in A)) \to A = On$

Metamath Proof Explorer

Theorem tfi

Proof