uzindi

Description: Indirect strong induction on the upper integers. (Contributed by Stefan O'Rear, 25-Aug-2015)

	Ref	Expression
Hypotheses	uzindi.a	$⊢ φ \to A \in V$
	uzindi.b	$⊢ φ \to T \in ℤ_{\geq L}$
	uzindi.c	$⊢ (φ \land R \in (L \dots T) \land \forall y (S \in (L ..^R) \to χ)) \to ψ$
	uzindi.d	$⊢ x = y \to (ψ \leftrightarrow χ)$
	uzindi.e	$⊢ x = A \to (ψ \leftrightarrow θ)$
	uzindi.f	$⊢ x = y \to R = S$
	uzindi.g	$⊢ x = A \to R = T$
Assertion	uzindi	$⊢ φ \to θ$

Proof

Step	Hyp	Ref	Expression
1		uzindi.a	$⊢ φ \to A \in V$
2		uzindi.b	$⊢ φ \to T \in ℤ_{\geq L}$
3		uzindi.c	$⊢ (φ \land R \in (L \dots T) \land \forall y (S \in (L ..^R) \to χ)) \to ψ$
4		uzindi.d	$⊢ x = y \to (ψ \leftrightarrow χ)$
5		uzindi.e	$⊢ x = A \to (ψ \leftrightarrow θ)$
6		uzindi.f	$⊢ x = y \to R = S$
7		uzindi.g	$⊢ x = A \to R = T$
8		eluzfz2	$⊢ T \in ℤ_{\geq L} \to T \in (L \dots T)$
9	2 8	syl	$⊢ φ \to T \in (L \dots T)$
10		fzofi	$⊢ (L ..^T) \in Fin$
11		finnum	$⊢ (L ..^T) \in Fin \to (L ..^T) \in dom card$
12	10 11	mp1i	$⊢ φ \to (L ..^T) \in dom card$
13		simpll	$⊢ ((φ \land \forall y ((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ))) \land R \in (L \dots T)) \to φ$
14		simpr	$⊢ ((φ \land \forall y ((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ))) \land R \in (L \dots T)) \to R \in (L \dots T)$
15		elfzuz3	$⊢ R \in (L \dots T) \to T \in ℤ_{\geq R}$
16	15	adantl	$⊢ (φ \land R \in (L \dots T)) \to T \in ℤ_{\geq R}$
17		fzoss2	$⊢ T \in ℤ_{\geq R} \to (L ..^R) \subseteq (L ..^T)$
18		fzossfz	$⊢ (L ..^T) \subseteq (L \dots T)$
19	17 18	sstrdi	$⊢ T \in ℤ_{\geq R} \to (L ..^R) \subseteq (L \dots T)$
20	16 19	syl	$⊢ (φ \land R \in (L \dots T)) \to (L ..^R) \subseteq (L \dots T)$
21	20	sselda	$⊢ ((φ \land R \in (L \dots T)) \land S \in (L ..^R)) \to S \in (L \dots T)$
22		fzofi	$⊢ (L ..^R) \in Fin$
23		elfzofz	$⊢ S \in (L ..^R) \to S \in (L \dots R)$
24	23	adantl	$⊢ ((φ \land R \in (L \dots T)) \land S \in (L ..^R)) \to S \in (L \dots R)$
25		elfzuz3	$⊢ S \in (L \dots R) \to R \in ℤ_{\geq S}$
26		fzoss2	$⊢ R \in ℤ_{\geq S} \to (L ..^S) \subseteq (L ..^R)$
27	24 25 26	3syl	$⊢ ((φ \land R \in (L \dots T)) \land S \in (L ..^R)) \to (L ..^S) \subseteq (L ..^R)$
28		fzonel	$⊢ \neg S \in (L ..^S)$
29	28	jctr	$⊢ S \in (L ..^R) \to (S \in (L ..^R) \land \neg S \in (L ..^S))$
30	29	adantl	$⊢ ((φ \land R \in (L \dots T)) \land S \in (L ..^R)) \to (S \in (L ..^R) \land \neg S \in (L ..^S))$
31		ssnelpss	$⊢ (L ..^S) \subseteq (L ..^R) \to ((S \in (L ..^R) \land \neg S \in (L ..^S)) \to (L ..^S) \subset (L ..^R))$
32	27 30 31	sylc	$⊢ ((φ \land R \in (L \dots T)) \land S \in (L ..^R)) \to (L ..^S) \subset (L ..^R)$
33		php3	$⊢ ((L ..^R) \in Fin \land (L ..^S) \subset (L ..^R)) \to (L ..^S) ≺ (L ..^R)$
34	22 32 33	sylancr	$⊢ ((φ \land R \in (L \dots T)) \land S \in (L ..^R)) \to (L ..^S) ≺ (L ..^R)$
35		id	$⊢ ((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ)) \to ((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ))$
36	35	com13	$⊢ S \in (L \dots T) \to ((L ..^S) ≺ (L ..^R) \to (((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ)) \to χ))$
37	21 34 36	sylc	$⊢ ((φ \land R \in (L \dots T)) \land S \in (L ..^R)) \to (((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ)) \to χ)$
38	37	ex	$⊢ (φ \land R \in (L \dots T)) \to (S \in (L ..^R) \to (((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ)) \to χ))$
39	38	com23	$⊢ (φ \land R \in (L \dots T)) \to (((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ)) \to (S \in (L ..^R) \to χ))$
40	39	alimdv	$⊢ (φ \land R \in (L \dots T)) \to (\forall y ((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ)) \to \forall y (S \in (L ..^R) \to χ))$
41	40	ex	$⊢ φ \to (R \in (L \dots T) \to (\forall y ((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ)) \to \forall y (S \in (L ..^R) \to χ)))$
42	41	com23	$⊢ φ \to (\forall y ((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ)) \to (R \in (L \dots T) \to \forall y (S \in (L ..^R) \to χ)))$
43	42	imp31	$⊢ ((φ \land \forall y ((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ))) \land R \in (L \dots T)) \to \forall y (S \in (L ..^R) \to χ)$
44	13 14 43 3	syl3anc	$⊢ ((φ \land \forall y ((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ))) \land R \in (L \dots T)) \to ψ$
45	44	ex	$⊢ (φ \land \forall y ((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ))) \to (R \in (L \dots T) \to ψ)$
46	45	3adant2	$⊢ (φ \land (L ..^R) ≼ (L ..^T) \land \forall y ((L ..^S) ≺ (L ..^R) \to (S \in (L \dots T) \to χ))) \to (R \in (L \dots T) \to ψ)$
47	6	eleq1d	$⊢ x = y \to (R \in (L \dots T) \leftrightarrow S \in (L \dots T))$
48	47 4	imbi12d	$⊢ x = y \to ((R \in (L \dots T) \to ψ) \leftrightarrow (S \in (L \dots T) \to χ))$
49	7	eleq1d	$⊢ x = A \to (R \in (L \dots T) \leftrightarrow T \in (L \dots T))$
50	49 5	imbi12d	$⊢ x = A \to ((R \in (L \dots T) \to ψ) \leftrightarrow (T \in (L \dots T) \to θ))$
51	6	oveq2d	$⊢ x = y \to (L ..^R) = (L ..^S)$
52	7	oveq2d	$⊢ x = A \to (L ..^R) = (L ..^T)$
53	1 12 46 48 50 51 52	indcardi	$⊢ φ \to (T \in (L \dots T) \to θ)$
54	9 53	mpd	$⊢ φ \to θ$

Metamath Proof Explorer

Theorem uzindi

Proof