rtrclind

Description: Principle of transitive induction. The first four hypotheses give various existences, the next four give necessary substitutions and the last two are the basis and the induction step. (Contributed by Drahflow, 12-Nov-2015)

	Ref	Expression
Hypotheses	rtrclind.1	$⊢ η \to Rel R$
	rtrclind.2	$⊢ η \to R \in V$
	rtrclind.3	$⊢ η \to S \in V$
	rtrclind.4	$⊢ η \to X \in V$
	rtrclind.5	$⊢ i = S \to (φ \leftrightarrow χ)$
	rtrclind.6	$⊢ i = x \to (φ \leftrightarrow ψ)$
	rtrclind.7	$⊢ i = j \to (φ \leftrightarrow θ)$
	rtrclind.8	$⊢ x = X \to (ψ \leftrightarrow τ)$
	rtrclind.9	$⊢ η \to χ$
	rtrclind.10	$⊢ η \to (j R x \to (θ \to ψ))$
Assertion	rtrclind	$⊢ η \to (S t* (R) X \to τ)$

Proof

Step	Hyp	Ref	Expression
1		rtrclind.1	$⊢ η \to Rel R$
2		rtrclind.2	$⊢ η \to R \in V$
3		rtrclind.3	$⊢ η \to S \in V$
4		rtrclind.4	$⊢ η \to X \in V$
5		rtrclind.5	$⊢ i = S \to (φ \leftrightarrow χ)$
6		rtrclind.6	$⊢ i = x \to (φ \leftrightarrow ψ)$
7		rtrclind.7	$⊢ i = j \to (φ \leftrightarrow θ)$
8		rtrclind.8	$⊢ x = X \to (ψ \leftrightarrow τ)$
9		rtrclind.9	$⊢ η \to χ$
10		rtrclind.10	$⊢ η \to (j R x \to (θ \to ψ))$
11	1 2	dfrtrcl2	$⊢ η \to t* (R) = t*rec (R)$
12	1 2	dfrtrclrec2	$⊢ η \to (S t*rec (R) X \leftrightarrow \exists n \in ℕ_{0} S (R ↑_{r} n) X)$
13	12	biimpac	$⊢ (S t*rec (R) X \land η) \to \exists n \in ℕ_{0} S (R ↑_{r} n) X$
14		simprl	$⊢ (S t*rec (R) X \land (η \land (S (R ↑_{r} n) X \land n \in ℕ_{0}))) \to η$
15		simprrr	$⊢ (S t*rec (R) X \land (η \land (S (R ↑_{r} n) X \land n \in ℕ_{0}))) \to n \in ℕ_{0}$
16		simprrl	$⊢ (S t*rec (R) X \land (η \land (S (R ↑_{r} n) X \land n \in ℕ_{0}))) \to S (R ↑_{r} n) X$
17	1 2 3 4 5 6 7 8 9 10	relexpind	$⊢ η \to (n \in ℕ_{0} \to (S (R ↑_{r} n) X \to τ))$
18	14 15 16 17	syl3c	$⊢ (S t*rec (R) X \land (η \land (S (R ↑_{r} n) X \land n \in ℕ_{0}))) \to τ$
19	18	anassrs	$⊢ ((S t*rec (R) X \land η) \land (S (R ↑_{r} n) X \land n \in ℕ_{0})) \to τ$
20	19	expcom	$⊢ (S (R ↑_{r} n) X \land n \in ℕ_{0}) \to ((S t*rec (R) X \land η) \to τ)$
21	20	expcom	$⊢ n \in ℕ_{0} \to (S (R ↑_{r} n) X \to ((S t*rec (R) X \land η) \to τ))$
22	21	rexlimiv	$⊢ \exists n \in ℕ_{0} S (R ↑_{r} n) X \to ((S t*rec (R) X \land η) \to τ)$
23	13 22	mpcom	$⊢ (S t*rec (R) X \land η) \to τ$
24	23	expcom	$⊢ η \to (S t*rec (R) X \to τ)$
25		breq	$⊢ t* (R) = trec (R) \to (S t (R) X \leftrightarrow S t*rec (R) X)$
26	25	imbi1d	$⊢ t* (R) = trec (R) \to ((S t (R) X \to τ) \leftrightarrow (S t*rec (R) X \to τ))$
27	24 26	syl5ibr	$⊢ t* (R) = trec (R) \to (η \to (S t (R) X \to τ))$
28	11 27	mpcom	$⊢ η \to (S t* (R) X \to τ)$

Metamath Proof Explorer

Theorem rtrclind

Proof