tfindsg2

Description: 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. The basis of this version is an arbitrary ordinal suc B instead of zero. (Contributed by NM, 5-Jan-2005) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		tfindsg2.1	$⊢ x = suc B \to (φ \leftrightarrow ψ)$
2		tfindsg2.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		tfindsg2.3	$⊢ x = suc y \to (φ \leftrightarrow θ)$
4		tfindsg2.4	$⊢ x = A \to (φ \leftrightarrow τ)$
5		tfindsg2.5	$⊢ B \in On \to ψ$
6		tfindsg2.6	$⊢ (y \in On \land B \in y) \to (χ \to θ)$
7		tfindsg2.7	$⊢ (Lim x \land B \in x) \to (\forall y \in x (B \in y \to χ) \to φ)$
8		onelon	$⊢ (A \in On \land B \in A) \to B \in On$
9		sucelon	$⊢ B \in On \leftrightarrow suc B \in On$
10	8 9	sylib	$⊢ (A \in On \land B \in A) \to suc B \in On$
11		eloni	$⊢ A \in On \to Ord A$
12		ordsucss	$⊢ Ord A \to (B \in A \to suc B \subseteq A)$
13	11 12	syl	$⊢ A \in On \to (B \in A \to suc B \subseteq A)$
14	13	imp	$⊢ (A \in On \land B \in A) \to suc B \subseteq A$
15	9 5	sylbir	$⊢ suc B \in On \to ψ$
16		eloni	$⊢ y \in On \to Ord y$
17		ordelsuc	$⊢ (B \in On \land Ord y) \to (B \in y \leftrightarrow suc B \subseteq y)$
18	16 17	sylan2	$⊢ (B \in On \land y \in On) \to (B \in y \leftrightarrow suc B \subseteq y)$
19	18	ancoms	$⊢ (y \in On \land B \in On) \to (B \in y \leftrightarrow suc B \subseteq y)$
20	6	ex	$⊢ y \in On \to (B \in y \to (χ \to θ))$
21	20	adantr	$⊢ (y \in On \land B \in On) \to (B \in y \to (χ \to θ))$
22	19 21	sylbird	$⊢ (y \in On \land B \in On) \to (suc B \subseteq y \to (χ \to θ))$
23	9 22	sylan2br	$⊢ (y \in On \land suc B \in On) \to (suc B \subseteq y \to (χ \to θ))$
24	23	imp	$⊢ ((y \in On \land suc B \in On) \land suc B \subseteq y) \to (χ \to θ)$
25	7	ex	$⊢ Lim x \to (B \in x \to (\forall y \in x (B \in y \to χ) \to φ))$
26	25	adantr	$⊢ (Lim x \land B \in On) \to (B \in x \to (\forall y \in x (B \in y \to χ) \to φ))$
27		vex	$⊢ x \in V$
28		limelon	$⊢ (x \in V \land Lim x) \to x \in On$
29	27 28	mpan	$⊢ Lim x \to x \in On$
30		eloni	$⊢ x \in On \to Ord x$
31		ordelsuc	$⊢ (B \in On \land Ord x) \to (B \in x \leftrightarrow suc B \subseteq x)$
32	30 31	sylan2	$⊢ (B \in On \land x \in On) \to (B \in x \leftrightarrow suc B \subseteq x)$
33		onelon	$⊢ (x \in On \land y \in x) \to y \in On$
34	33 16	syl	$⊢ (x \in On \land y \in x) \to Ord y$
35	34 17	sylan2	$⊢ (B \in On \land (x \in On \land y \in x)) \to (B \in y \leftrightarrow suc B \subseteq y)$
36	35	anassrs	$⊢ ((B \in On \land x \in On) \land y \in x) \to (B \in y \leftrightarrow suc B \subseteq y)$
37	36	imbi1d	$⊢ ((B \in On \land x \in On) \land y \in x) \to ((B \in y \to χ) \leftrightarrow (suc B \subseteq y \to χ))$
38	37	ralbidva	$⊢ (B \in On \land x \in On) \to (\forall y \in x (B \in y \to χ) \leftrightarrow \forall y \in x (suc B \subseteq y \to χ))$
39	38	imbi1d	$⊢ (B \in On \land x \in On) \to ((\forall y \in x (B \in y \to χ) \to φ) \leftrightarrow (\forall y \in x (suc B \subseteq y \to χ) \to φ))$
40	32 39	imbi12d	$⊢ (B \in On \land x \in On) \to ((B \in x \to (\forall y \in x (B \in y \to χ) \to φ)) \leftrightarrow (suc B \subseteq x \to (\forall y \in x (suc B \subseteq y \to χ) \to φ)))$
41	29 40	sylan2	$⊢ (B \in On \land Lim x) \to ((B \in x \to (\forall y \in x (B \in y \to χ) \to φ)) \leftrightarrow (suc B \subseteq x \to (\forall y \in x (suc B \subseteq y \to χ) \to φ)))$
42	41	ancoms	$⊢ (Lim x \land B \in On) \to ((B \in x \to (\forall y \in x (B \in y \to χ) \to φ)) \leftrightarrow (suc B \subseteq x \to (\forall y \in x (suc B \subseteq y \to χ) \to φ)))$
43	26 42	mpbid	$⊢ (Lim x \land B \in On) \to (suc B \subseteq x \to (\forall y \in x (suc B \subseteq y \to χ) \to φ))$
44	9 43	sylan2br	$⊢ (Lim x \land suc B \in On) \to (suc B \subseteq x \to (\forall y \in x (suc B \subseteq y \to χ) \to φ))$
45	44	imp	$⊢ ((Lim x \land suc B \in On) \land suc B \subseteq x) \to (\forall y \in x (suc B \subseteq y \to χ) \to φ)$
46	1 2 3 4 15 24 45	tfindsg	$⊢ ((A \in On \land suc B \in On) \land suc B \subseteq A) \to τ$
47	46	expl	$⊢ A \in On \to ((suc B \in On \land suc B \subseteq A) \to τ)$
48	47	adantr	$⊢ (A \in On \land B \in A) \to ((suc B \in On \land suc B \subseteq A) \to τ)$
49	10 14 48	mp2and	$⊢ (A \in On \land B \in A) \to τ$

Metamath Proof Explorer

Theorem tfindsg2

Proof