This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑌 ‘ 𝑏 ) ) )