tfinds

Description: Principle of Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. Theorem Schema 4 of Suppes p. 197. (Contributed by NM, 16-Apr-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Hypotheses	tfinds.1	$⊢ x = \emptyset \to (φ \leftrightarrow ψ)$
	tfinds.2	$⊢ x = y \to (φ \leftrightarrow χ)$
	tfinds.3	$⊢ x = suc y \to (φ \leftrightarrow θ)$
	tfinds.4	$⊢ x = A \to (φ \leftrightarrow τ)$
	tfinds.5	$⊢ ψ$
	tfinds.6	$⊢ y \in On \to (χ \to θ)$
	tfinds.7	$⊢ Lim x \to (\forall y \in x χ \to φ)$
Assertion	tfinds	$⊢ A \in On \to τ$

Proof

Step	Hyp	Ref	Expression
1		tfinds.1	$⊢ x = \emptyset \to (φ \leftrightarrow ψ)$
2		tfinds.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		tfinds.3	$⊢ x = suc y \to (φ \leftrightarrow θ)$
4		tfinds.4	$⊢ x = A \to (φ \leftrightarrow τ)$
5		tfinds.5	$⊢ ψ$
6		tfinds.6	$⊢ y \in On \to (χ \to θ)$
7		tfinds.7	$⊢ Lim x \to (\forall y \in x χ \to φ)$
8		dflim3	$⊢ Lim x \leftrightarrow (Ord x \land \neg (x = \emptyset \lor \exists y \in On x = suc y))$
9	8	notbii	$⊢ \neg Lim x \leftrightarrow \neg (Ord x \land \neg (x = \emptyset \lor \exists y \in On x = suc y))$
10		iman	$⊢ (Ord x \to (x = \emptyset \lor \exists y \in On x = suc y)) \leftrightarrow \neg (Ord x \land \neg (x = \emptyset \lor \exists y \in On x = suc y))$
11		eloni	$⊢ x \in On \to Ord x$
12		pm2.27	$⊢ Ord x \to ((Ord x \to (x = \emptyset \lor \exists y \in On x = suc y)) \to (x = \emptyset \lor \exists y \in On x = suc y))$
13	11 12	syl	$⊢ x \in On \to ((Ord x \to (x = \emptyset \lor \exists y \in On x = suc y)) \to (x = \emptyset \lor \exists y \in On x = suc y))$
14	5 1	mpbiri	$⊢ x = \emptyset \to φ$
15	14	a1d	$⊢ x = \emptyset \to (\forall y \in x χ \to φ)$
16		nfra1	$⊢ Ⅎ y \forall y \in x χ$
17		nfv	$⊢ Ⅎ y φ$
18	16 17	nfim	$⊢ Ⅎ y (\forall y \in x χ \to φ)$
19		vex	$⊢ y \in V$
20	19	sucid	$⊢ y \in suc y$
21	2	rspcv	$⊢ y \in suc y \to (\forall x \in suc y φ \to χ)$
22	20 21	ax-mp	$⊢ \forall x \in suc y φ \to χ$
23	22 6	syl5	$⊢ y \in On \to (\forall x \in suc y φ \to θ)$
24		raleq	$⊢ x = suc y \to (\forall z \in x [z/ x] φ \leftrightarrow \forall z \in suc y [z/ x] φ)$
25		nfv	$⊢ Ⅎ x χ$
26	25 2	sbiev	$⊢ [y/ x] φ \leftrightarrow χ$
27		sbequ	$⊢ y = z \to ([y/ x] φ \leftrightarrow [z/ x] φ)$
28	26 27	bitr3id	$⊢ y = z \to (χ \leftrightarrow [z/ x] φ)$
29	28	cbvralvw	$⊢ \forall y \in x χ \leftrightarrow \forall z \in x [z/ x] φ$
30		cbvralsvw	$⊢ \forall x \in suc y φ \leftrightarrow \forall z \in suc y [z/ x] φ$
31	24 29 30	3bitr4g	$⊢ x = suc y \to (\forall y \in x χ \leftrightarrow \forall x \in suc y φ)$
32	31	imbi1d	$⊢ x = suc y \to ((\forall y \in x χ \to θ) \leftrightarrow (\forall x \in suc y φ \to θ))$
33	23 32	syl5ibrcom	$⊢ y \in On \to (x = suc y \to (\forall y \in x χ \to θ))$
34	3	biimprd	$⊢ x = suc y \to (θ \to φ)$
35	34	a1i	$⊢ y \in On \to (x = suc y \to (θ \to φ))$
36	33 35	syldd	$⊢ y \in On \to (x = suc y \to (\forall y \in x χ \to φ))$
37	18 36	rexlimi	$⊢ \exists y \in On x = suc y \to (\forall y \in x χ \to φ)$
38	15 37	jaoi	$⊢ (x = \emptyset \lor \exists y \in On x = suc y) \to (\forall y \in x χ \to φ)$
39	13 38	syl6	$⊢ x \in On \to ((Ord x \to (x = \emptyset \lor \exists y \in On x = suc y)) \to (\forall y \in x χ \to φ))$
40	10 39	syl5bir	$⊢ x \in On \to (\neg (Ord x \land \neg (x = \emptyset \lor \exists y \in On x = suc y)) \to (\forall y \in x χ \to φ))$
41	9 40	syl5bi	$⊢ x \in On \to (\neg Lim x \to (\forall y \in x χ \to φ))$
42	41 7	pm2.61d2	$⊢ x \in On \to (\forall y \in x χ \to φ)$
43	2 4 42	tfis3	$⊢ A \in On \to τ$

Metamath Proof Explorer

Theorem tfinds

Proof