Theorem fin23lem38

Description: Lemma for fin23 . The contradictory chain has no minimum. (Contributed by Stefan O'Rear, 2-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

	Ref	Expression
Hypotheses	fin23lem33.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
	fin23lem.f	⊢ ( 𝜑 → ℎ : ω –1-1→ V )
	fin23lem.g	⊢ ( 𝜑 → ∪ ran ℎ ⊆ 𝐺 )
	fin23lem.h	⊢ ( 𝜑 → ∀ 𝑗 ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) )
	fin23lem.i	⊢ 𝑌 = ( rec ( 𝑖 , ℎ ) ↾ ω )
Assertion	fin23lem38	⊢ ( 𝜑 → ¬ ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ∈ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fin23lem33.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
2		fin23lem.f	⊢ ( 𝜑 → ℎ : ω –1-1→ V )
3		fin23lem.g	⊢ ( 𝜑 → ∪ ran ℎ ⊆ 𝐺 )
4		fin23lem.h	⊢ ( 𝜑 → ∀ 𝑗 ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) )
5		fin23lem.i	⊢ 𝑌 = ( rec ( 𝑖 , ℎ ) ↾ ω )
6		peano2	⊢ ( 𝑑 ∈ ω → suc 𝑑 ∈ ω )
7		eqid	⊢ ∪ ran ( 𝑌 ‘ suc 𝑑 ) = ∪ ran ( 𝑌 ‘ suc 𝑑 )
8		fveq2	⊢ ( 𝑏 = suc 𝑑 → ( 𝑌 ‘ 𝑏 ) = ( 𝑌 ‘ suc 𝑑 ) )
9	8	rneqd	⊢ ( 𝑏 = suc 𝑑 → ran ( 𝑌 ‘ 𝑏 ) = ran ( 𝑌 ‘ suc 𝑑 ) )
10	9	unieqd	⊢ ( 𝑏 = suc 𝑑 → ∪ ran ( 𝑌 ‘ 𝑏 ) = ∪ ran ( 𝑌 ‘ suc 𝑑 ) )
11	10	rspceeqv	⊢ ( ( suc 𝑑 ∈ ω ∧ ∪ ran ( 𝑌 ‘ suc 𝑑 ) = ∪ ran ( 𝑌 ‘ suc 𝑑 ) ) → ∃ 𝑏 ∈ ω ∪ ran ( 𝑌 ‘ suc 𝑑 ) = ∪ ran ( 𝑌 ‘ 𝑏 ) )
12	7 11	mpan2	⊢ ( suc 𝑑 ∈ ω → ∃ 𝑏 ∈ ω ∪ ran ( 𝑌 ‘ suc 𝑑 ) = ∪ ran ( 𝑌 ‘ 𝑏 ) )
13		fvex	⊢ ( 𝑌 ‘ suc 𝑑 ) ∈ V
14	13	rnex	⊢ ran ( 𝑌 ‘ suc 𝑑 ) ∈ V
15	14	uniex	⊢ ∪ ran ( 𝑌 ‘ suc 𝑑 ) ∈ V
16		eqid	⊢ ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) = ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) )
17	16	elrnmpt	⊢ ( ∪ ran ( 𝑌 ‘ suc 𝑑 ) ∈ V → ( ∪ ran ( 𝑌 ‘ suc 𝑑 ) ∈ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ↔ ∃ 𝑏 ∈ ω ∪ ran ( 𝑌 ‘ suc 𝑑 ) = ∪ ran ( 𝑌 ‘ 𝑏 ) ) )
18	15 17	ax-mp	⊢ ( ∪ ran ( 𝑌 ‘ suc 𝑑 ) ∈ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ↔ ∃ 𝑏 ∈ ω ∪ ran ( 𝑌 ‘ suc 𝑑 ) = ∪ ran ( 𝑌 ‘ 𝑏 ) )
19	12 18	sylibr	⊢ ( suc 𝑑 ∈ ω → ∪ ran ( 𝑌 ‘ suc 𝑑 ) ∈ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) )
20	6 19	syl	⊢ ( 𝑑 ∈ ω → ∪ ran ( 𝑌 ‘ suc 𝑑 ) ∈ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ω ) → ∪ ran ( 𝑌 ‘ suc 𝑑 ) ∈ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) )
22		intss1	⊢ ( ∪ ran ( 𝑌 ‘ suc 𝑑 ) ∈ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) → ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ⊆ ∪ ran ( 𝑌 ‘ suc 𝑑 ) )
23	21 22	syl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ω ) → ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ⊆ ∪ ran ( 𝑌 ‘ suc 𝑑 ) )
24	1 2 3 4 5	fin23lem35	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ω ) → ∪ ran ( 𝑌 ‘ suc 𝑑 ) ⊊ ∪ ran ( 𝑌 ‘ 𝑑 ) )
25	23 24	sspsstrd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ω ) → ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑑 ) )
26		dfpss2	⊢ ( ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑑 ) ↔ ( ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ⊆ ∪ ran ( 𝑌 ‘ 𝑑 ) ∧ ¬ ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) = ∪ ran ( 𝑌 ‘ 𝑑 ) ) )
27	26	simprbi	⊢ ( ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑑 ) → ¬ ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) = ∪ ran ( 𝑌 ‘ 𝑑 ) )
28	25 27	syl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ω ) → ¬ ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) = ∪ ran ( 𝑌 ‘ 𝑑 ) )
29	28	nrexdv	⊢ ( 𝜑 → ¬ ∃ 𝑑 ∈ ω ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) = ∪ ran ( 𝑌 ‘ 𝑑 ) )
30		fveq2	⊢ ( 𝑏 = 𝑑 → ( 𝑌 ‘ 𝑏 ) = ( 𝑌 ‘ 𝑑 ) )
31	30	rneqd	⊢ ( 𝑏 = 𝑑 → ran ( 𝑌 ‘ 𝑏 ) = ran ( 𝑌 ‘ 𝑑 ) )
32	31	unieqd	⊢ ( 𝑏 = 𝑑 → ∪ ran ( 𝑌 ‘ 𝑏 ) = ∪ ran ( 𝑌 ‘ 𝑑 ) )
33	32	cbvmptv	⊢ ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) = ( 𝑑 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑑 ) )
34	33	elrnmpt	⊢ ( ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ∈ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) → ( ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ∈ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ↔ ∃ 𝑑 ∈ ω ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) = ∪ ran ( 𝑌 ‘ 𝑑 ) ) )
35	34	ibi	⊢ ( ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ∈ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) → ∃ 𝑑 ∈ ω ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) = ∪ ran ( 𝑌 ‘ 𝑑 ) )
36	29 35	nsyl	⊢ ( 𝜑 → ¬ ∩ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ∈ ran ( 𝑏 ∈ ω ↦ ∪ ran ( 𝑌 ‘ 𝑏 ) ) )