tfindsg

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 B instead of zero. Remark in TakeutiZaring p. 57. (Contributed by NM, 5-Mar-2004)

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

Proof

Step	Hyp	Ref	Expression
1		tfindsg.1	$⊢ x = B \to (φ \leftrightarrow ψ)$
2		tfindsg.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		tfindsg.3	$⊢ x = suc y \to (φ \leftrightarrow θ)$
4		tfindsg.4	$⊢ x = A \to (φ \leftrightarrow τ)$
5		tfindsg.5	$⊢ B \in On \to ψ$
6		tfindsg.6	$⊢ ((y \in On \land B \in On) \land B \subseteq y) \to (χ \to θ)$
7		tfindsg.7	$⊢ ((Lim x \land B \in On) \land B \subseteq x) \to (\forall y \in x (B \subseteq y \to χ) \to φ)$
8		sseq2	$⊢ x = \emptyset \to (B \subseteq x \leftrightarrow B \subseteq \emptyset)$
9	8	adantl	$⊢ (B = \emptyset \land x = \emptyset) \to (B \subseteq x \leftrightarrow B \subseteq \emptyset)$
10		eqeq2	$⊢ B = \emptyset \to (x = B \leftrightarrow x = \emptyset)$
11	10 1	syl6bir	$⊢ B = \emptyset \to (x = \emptyset \to (φ \leftrightarrow ψ))$
12	11	imp	$⊢ (B = \emptyset \land x = \emptyset) \to (φ \leftrightarrow ψ)$
13	9 12	imbi12d	$⊢ (B = \emptyset \land x = \emptyset) \to ((B \subseteq x \to φ) \leftrightarrow (B \subseteq \emptyset \to ψ))$
14	8	imbi1d	$⊢ x = \emptyset \to ((B \subseteq x \to φ) \leftrightarrow (B \subseteq \emptyset \to φ))$
15		ss0	$⊢ B \subseteq \emptyset \to B = \emptyset$
16	15	con3i	$⊢ \neg B = \emptyset \to \neg B \subseteq \emptyset$
17	16	pm2.21d	$⊢ \neg B = \emptyset \to (B \subseteq \emptyset \to (φ \leftrightarrow ψ))$
18	17	pm5.74d	$⊢ \neg B = \emptyset \to ((B \subseteq \emptyset \to φ) \leftrightarrow (B \subseteq \emptyset \to ψ))$
19	14 18	sylan9bbr	$⊢ (\neg B = \emptyset \land x = \emptyset) \to ((B \subseteq x \to φ) \leftrightarrow (B \subseteq \emptyset \to ψ))$
20	13 19	pm2.61ian	$⊢ x = \emptyset \to ((B \subseteq x \to φ) \leftrightarrow (B \subseteq \emptyset \to ψ))$
21	20	imbi2d	$⊢ x = \emptyset \to ((B \in On \to (B \subseteq x \to φ)) \leftrightarrow (B \in On \to (B \subseteq \emptyset \to ψ)))$
22		sseq2	$⊢ x = y \to (B \subseteq x \leftrightarrow B \subseteq y)$
23	22 2	imbi12d	$⊢ x = y \to ((B \subseteq x \to φ) \leftrightarrow (B \subseteq y \to χ))$
24	23	imbi2d	$⊢ x = y \to ((B \in On \to (B \subseteq x \to φ)) \leftrightarrow (B \in On \to (B \subseteq y \to χ)))$
25		sseq2	$⊢ x = suc y \to (B \subseteq x \leftrightarrow B \subseteq suc y)$
26	25 3	imbi12d	$⊢ x = suc y \to ((B \subseteq x \to φ) \leftrightarrow (B \subseteq suc y \to θ))$
27	26	imbi2d	$⊢ x = suc y \to ((B \in On \to (B \subseteq x \to φ)) \leftrightarrow (B \in On \to (B \subseteq suc y \to θ)))$
28		sseq2	$⊢ x = A \to (B \subseteq x \leftrightarrow B \subseteq A)$
29	28 4	imbi12d	$⊢ x = A \to ((B \subseteq x \to φ) \leftrightarrow (B \subseteq A \to τ))$
30	29	imbi2d	$⊢ x = A \to ((B \in On \to (B \subseteq x \to φ)) \leftrightarrow (B \in On \to (B \subseteq A \to τ)))$
31	5	a1d	$⊢ B \in On \to (B \subseteq \emptyset \to ψ)$
32		vex	$⊢ y \in V$
33	32	sucex	$⊢ suc y \in V$
34	33	eqvinc	$⊢ suc y = B \leftrightarrow \exists x (x = suc y \land x = B)$
35	5 1	syl5ibr	$⊢ x = B \to (B \in On \to φ)$
36	3	biimpd	$⊢ x = suc y \to (φ \to θ)$
37	35 36	sylan9r	$⊢ (x = suc y \land x = B) \to (B \in On \to θ)$
38	37	exlimiv	$⊢ \exists x (x = suc y \land x = B) \to (B \in On \to θ)$
39	34 38	sylbi	$⊢ suc y = B \to (B \in On \to θ)$
40	39	eqcoms	$⊢ B = suc y \to (B \in On \to θ)$
41	40	imim2i	$⊢ (B \subseteq suc y \to B = suc y) \to (B \subseteq suc y \to (B \in On \to θ))$
42	41	a1d	$⊢ (B \subseteq suc y \to B = suc y) \to ((B \subseteq y \to χ) \to (B \subseteq suc y \to (B \in On \to θ)))$
43	42	com4r	$⊢ B \in On \to ((B \subseteq suc y \to B = suc y) \to ((B \subseteq y \to χ) \to (B \subseteq suc y \to θ)))$
44	43	adantl	$⊢ (y \in On \land B \in On) \to ((B \subseteq suc y \to B = suc y) \to ((B \subseteq y \to χ) \to (B \subseteq suc y \to θ)))$
45		df-ne	$⊢ B \neq suc y \leftrightarrow \neg B = suc y$
46	45	anbi2i	$⊢ (B \subseteq suc y \land B \neq suc y) \leftrightarrow (B \subseteq suc y \land \neg B = suc y)$
47		annim	$⊢ (B \subseteq suc y \land \neg B = suc y) \leftrightarrow \neg (B \subseteq suc y \to B = suc y)$
48	46 47	bitri	$⊢ (B \subseteq suc y \land B \neq suc y) \leftrightarrow \neg (B \subseteq suc y \to B = suc y)$
49		onsssuc	$⊢ (B \in On \land y \in On) \to (B \subseteq y \leftrightarrow B \in suc y)$
50		suceloni	$⊢ y \in On \to suc y \in On$
51		onelpss	$⊢ (B \in On \land suc y \in On) \to (B \in suc y \leftrightarrow (B \subseteq suc y \land B \neq suc y))$
52	50 51	sylan2	$⊢ (B \in On \land y \in On) \to (B \in suc y \leftrightarrow (B \subseteq suc y \land B \neq suc y))$
53	49 52	bitrd	$⊢ (B \in On \land y \in On) \to (B \subseteq y \leftrightarrow (B \subseteq suc y \land B \neq suc y))$
54	53	ancoms	$⊢ (y \in On \land B \in On) \to (B \subseteq y \leftrightarrow (B \subseteq suc y \land B \neq suc y))$
55	6	ex	$⊢ (y \in On \land B \in On) \to (B \subseteq y \to (χ \to θ))$
56	55	a1ddd	$⊢ (y \in On \land B \in On) \to (B \subseteq y \to (χ \to (B \subseteq suc y \to θ)))$
57	56	a2d	$⊢ (y \in On \land B \in On) \to ((B \subseteq y \to χ) \to (B \subseteq y \to (B \subseteq suc y \to θ)))$
58	57	com23	$⊢ (y \in On \land B \in On) \to (B \subseteq y \to ((B \subseteq y \to χ) \to (B \subseteq suc y \to θ)))$
59	54 58	sylbird	$⊢ (y \in On \land B \in On) \to ((B \subseteq suc y \land B \neq suc y) \to ((B \subseteq y \to χ) \to (B \subseteq suc y \to θ)))$
60	48 59	syl5bir	$⊢ (y \in On \land B \in On) \to (\neg (B \subseteq suc y \to B = suc y) \to ((B \subseteq y \to χ) \to (B \subseteq suc y \to θ)))$
61	44 60	pm2.61d	$⊢ (y \in On \land B \in On) \to ((B \subseteq y \to χ) \to (B \subseteq suc y \to θ))$
62	61	ex	$⊢ y \in On \to (B \in On \to ((B \subseteq y \to χ) \to (B \subseteq suc y \to θ)))$
63	62	a2d	$⊢ y \in On \to ((B \in On \to (B \subseteq y \to χ)) \to (B \in On \to (B \subseteq suc y \to θ)))$
64		pm2.27	$⊢ B \in On \to ((B \in On \to (B \subseteq y \to χ)) \to (B \subseteq y \to χ))$
65	64	ralimdv	$⊢ B \in On \to (\forall y \in x (B \in On \to (B \subseteq y \to χ)) \to \forall y \in x (B \subseteq y \to χ))$
66	65	ad2antlr	$⊢ ((Lim x \land B \in On) \land B \subseteq x) \to (\forall y \in x (B \in On \to (B \subseteq y \to χ)) \to \forall y \in x (B \subseteq y \to χ))$
67	66 7	syld	$⊢ ((Lim x \land B \in On) \land B \subseteq x) \to (\forall y \in x (B \in On \to (B \subseteq y \to χ)) \to φ)$
68	67	exp31	$⊢ Lim x \to (B \in On \to (B \subseteq x \to (\forall y \in x (B \in On \to (B \subseteq y \to χ)) \to φ)))$
69	68	com3l	$⊢ B \in On \to (B \subseteq x \to (Lim x \to (\forall y \in x (B \in On \to (B \subseteq y \to χ)) \to φ)))$
70	69	com4t	$⊢ Lim x \to (\forall y \in x (B \in On \to (B \subseteq y \to χ)) \to (B \in On \to (B \subseteq x \to φ)))$
71	21 24 27 30 31 63 70	tfinds	$⊢ A \in On \to (B \in On \to (B \subseteq A \to τ))$
72	71	imp31	$⊢ ((A \in On \land B \in On) \land B \subseteq A) \to τ$

Metamath Proof Explorer

Theorem tfindsg

Proof