uzindi

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

	Ref	Expression
Hypotheses	uzindi.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	uzindi.b	⊢ ( 𝜑 → 𝑇 ∈ ( ℤ_≥ ‘ 𝐿 ) )
	uzindi.c	⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ∧ ∀ 𝑦 ( 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) → 𝜒 ) ) → 𝜓 )
	uzindi.d	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
	uzindi.e	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜃 ) )
	uzindi.f	⊢ ( 𝑥 = 𝑦 → 𝑅 = 𝑆 )
	uzindi.g	⊢ ( 𝑥 = 𝐴 → 𝑅 = 𝑇 )
Assertion	uzindi	⊢ ( 𝜑 → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		uzindi.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		uzindi.b	⊢ ( 𝜑 → 𝑇 ∈ ( ℤ_≥ ‘ 𝐿 ) )
3		uzindi.c	⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ∧ ∀ 𝑦 ( 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) → 𝜒 ) ) → 𝜓 )
4		uzindi.d	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
5		uzindi.e	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜃 ) )
6		uzindi.f	⊢ ( 𝑥 = 𝑦 → 𝑅 = 𝑆 )
7		uzindi.g	⊢ ( 𝑥 = 𝐴 → 𝑅 = 𝑇 )
8		eluzfz2	⊢ ( 𝑇 ∈ ( ℤ_≥ ‘ 𝐿 ) → 𝑇 ∈ ( 𝐿 ... 𝑇 ) )
9	2 8	syl	⊢ ( 𝜑 → 𝑇 ∈ ( 𝐿 ... 𝑇 ) )
10		fzofi	⊢ ( 𝐿 ..^ 𝑇 ) ∈ Fin
11		finnum	⊢ ( ( 𝐿 ..^ 𝑇 ) ∈ Fin → ( 𝐿 ..^ 𝑇 ) ∈ dom card )
12	10 11	mp1i	⊢ ( 𝜑 → ( 𝐿 ..^ 𝑇 ) ∈ dom card )
13		simpll	⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) → 𝜑 )
14		simpr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) → 𝑅 ∈ ( 𝐿 ... 𝑇 ) )
15		elfzuz3	⊢ ( 𝑅 ∈ ( 𝐿 ... 𝑇 ) → 𝑇 ∈ ( ℤ_≥ ‘ 𝑅 ) )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) → 𝑇 ∈ ( ℤ_≥ ‘ 𝑅 ) )
17		fzoss2	⊢ ( 𝑇 ∈ ( ℤ_≥ ‘ 𝑅 ) → ( 𝐿 ..^ 𝑅 ) ⊆ ( 𝐿 ..^ 𝑇 ) )
18		fzossfz	⊢ ( 𝐿 ..^ 𝑇 ) ⊆ ( 𝐿 ... 𝑇 )
19	17 18	sstrdi	⊢ ( 𝑇 ∈ ( ℤ_≥ ‘ 𝑅 ) → ( 𝐿 ..^ 𝑅 ) ⊆ ( 𝐿 ... 𝑇 ) )
20	16 19	syl	⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) → ( 𝐿 ..^ 𝑅 ) ⊆ ( 𝐿 ... 𝑇 ) )
21	20	sselda	⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) ∧ 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) ) → 𝑆 ∈ ( 𝐿 ... 𝑇 ) )
22		fzofi	⊢ ( 𝐿 ..^ 𝑅 ) ∈ Fin
23		elfzofz	⊢ ( 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) → 𝑆 ∈ ( 𝐿 ... 𝑅 ) )
24	23	adantl	⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) ∧ 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) ) → 𝑆 ∈ ( 𝐿 ... 𝑅 ) )
25		elfzuz3	⊢ ( 𝑆 ∈ ( 𝐿 ... 𝑅 ) → 𝑅 ∈ ( ℤ_≥ ‘ 𝑆 ) )
26		fzoss2	⊢ ( 𝑅 ∈ ( ℤ_≥ ‘ 𝑆 ) → ( 𝐿 ..^ 𝑆 ) ⊆ ( 𝐿 ..^ 𝑅 ) )
27	24 25 26	3syl	⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) ∧ 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) ) → ( 𝐿 ..^ 𝑆 ) ⊆ ( 𝐿 ..^ 𝑅 ) )
28		fzonel	⊢ ¬ 𝑆 ∈ ( 𝐿 ..^ 𝑆 )
29	28	jctr	⊢ ( 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) ∧ ¬ 𝑆 ∈ ( 𝐿 ..^ 𝑆 ) ) )
30	29	adantl	⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) ∧ 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) ) → ( 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) ∧ ¬ 𝑆 ∈ ( 𝐿 ..^ 𝑆 ) ) )
31		ssnelpss	⊢ ( ( 𝐿 ..^ 𝑆 ) ⊆ ( 𝐿 ..^ 𝑅 ) → ( ( 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) ∧ ¬ 𝑆 ∈ ( 𝐿 ..^ 𝑆 ) ) → ( 𝐿 ..^ 𝑆 ) ⊊ ( 𝐿 ..^ 𝑅 ) ) )
32	27 30 31	sylc	⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) ∧ 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) ) → ( 𝐿 ..^ 𝑆 ) ⊊ ( 𝐿 ..^ 𝑅 ) )
33		php3	⊢ ( ( ( 𝐿 ..^ 𝑅 ) ∈ Fin ∧ ( 𝐿 ..^ 𝑆 ) ⊊ ( 𝐿 ..^ 𝑅 ) ) → ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) )
34	22 32 33	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) ∧ 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) ) → ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) )
35		id	⊢ ( ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) → ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) )
36	35	com13	⊢ ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) → 𝜒 ) ) )
37	21 34 36	sylc	⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) ∧ 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) ) → ( ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) → 𝜒 ) )
38	37	ex	⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) → ( 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) → ( ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) → 𝜒 ) ) )
39	38	com23	⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) → ( ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) → ( 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) → 𝜒 ) ) )
40	39	alimdv	⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) → ( ∀ 𝑦 ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) → ∀ 𝑦 ( 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) → 𝜒 ) ) )
41	40	ex	⊢ ( 𝜑 → ( 𝑅 ∈ ( 𝐿 ... 𝑇 ) → ( ∀ 𝑦 ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) → ∀ 𝑦 ( 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) → 𝜒 ) ) ) )
42	41	com23	⊢ ( 𝜑 → ( ∀ 𝑦 ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) → ( 𝑅 ∈ ( 𝐿 ... 𝑇 ) → ∀ 𝑦 ( 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) → 𝜒 ) ) ) )
43	42	imp31	⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) → ∀ 𝑦 ( 𝑆 ∈ ( 𝐿 ..^ 𝑅 ) → 𝜒 ) )
44	13 14 43 3	syl3anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) ) ∧ 𝑅 ∈ ( 𝐿 ... 𝑇 ) ) → 𝜓 )
45	44	ex	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) ) → ( 𝑅 ∈ ( 𝐿 ... 𝑇 ) → 𝜓 ) )
46	45	3adant2	⊢ ( ( 𝜑 ∧ ( 𝐿 ..^ 𝑅 ) ≼ ( 𝐿 ..^ 𝑇 ) ∧ ∀ 𝑦 ( ( 𝐿 ..^ 𝑆 ) ≺ ( 𝐿 ..^ 𝑅 ) → ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) ) → ( 𝑅 ∈ ( 𝐿 ... 𝑇 ) → 𝜓 ) )
47	6	eleq1d	⊢ ( 𝑥 = 𝑦 → ( 𝑅 ∈ ( 𝐿 ... 𝑇 ) ↔ 𝑆 ∈ ( 𝐿 ... 𝑇 ) ) )
48	47 4	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑅 ∈ ( 𝐿 ... 𝑇 ) → 𝜓 ) ↔ ( 𝑆 ∈ ( 𝐿 ... 𝑇 ) → 𝜒 ) ) )
49	7	eleq1d	⊢ ( 𝑥 = 𝐴 → ( 𝑅 ∈ ( 𝐿 ... 𝑇 ) ↔ 𝑇 ∈ ( 𝐿 ... 𝑇 ) ) )
50	49 5	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑅 ∈ ( 𝐿 ... 𝑇 ) → 𝜓 ) ↔ ( 𝑇 ∈ ( 𝐿 ... 𝑇 ) → 𝜃 ) ) )
51	6	oveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐿 ..^ 𝑅 ) = ( 𝐿 ..^ 𝑆 ) )
52	7	oveq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐿 ..^ 𝑅 ) = ( 𝐿 ..^ 𝑇 ) )
53	1 12 46 48 50 51 52	indcardi	⊢ ( 𝜑 → ( 𝑇 ∈ ( 𝐿 ... 𝑇 ) → 𝜃 ) )
54	9 53	mpd	⊢ ( 𝜑 → 𝜃 )

Metamath Proof Explorer

Theorem uzindi

Proof