Metamath Proof Explorer

Theorem isf32lem5

Description: Lemma for isfin3-2 . There are infinite decrease points. (Contributed by Stefan O'Rear, 5-Nov-2014)

Ref Expression
Hypotheses isf32lem.a ⊢ ( 𝜑 → 𝐹 : ω ⟶ 𝒫 𝐺 )
isf32lem.b ⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
isf32lem.c ⊢ ( 𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹 )
isf32lem.d ⊢ 𝑆 = { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹 ‘ 𝑦 ) }
Assertion isf32lem5 ( 𝜑 → ¬ 𝑆 ∈ Fin )

Proof

Step Hyp Ref Expression
1 isf32lem.a ⊢ ( 𝜑 → 𝐹 : ω ⟶ 𝒫 𝐺 )
2 isf32lem.b ⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
3 isf32lem.c ⊢ ( 𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹 )
4 isf32lem.d ⊢ 𝑆 = { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹 ‘ 𝑦 ) }
5 1 2 3 isf32lem2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ω ) → ∃ 𝑏 ∈ ω ( 𝑎 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) )
6 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ω ∃ 𝑏 ∈ ω ( 𝑎 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) )
7 4 ssrab3 ⊢ 𝑆 ⊆ ω
8 nnunifi ⊢ ( ( 𝑆 ⊆ ω ∧ 𝑆 ∈ Fin ) → ∪ 𝑆 ∈ ω )
9 7 8 mpan ⊢ ( 𝑆 ∈ Fin → ∪ 𝑆 ∈ ω )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑆 ∈ Fin ) → ∪ 𝑆 ∈ ω )
11 elssuni ⊢ ( 𝑏 ∈ 𝑆 → 𝑏 ⊆ ∪ 𝑆 )
12 nnon ⊢ ( 𝑏 ∈ ω → 𝑏 ∈ On )
13 omsson ⊢ ω ⊆ On
14 13 10 sseldi ⊢ ( ( 𝜑 ∧ 𝑆 ∈ Fin ) → ∪ 𝑆 ∈ On )
15 ontri1 ⊢ ( ( 𝑏 ∈ On ∧ ∪ 𝑆 ∈ On ) → ( 𝑏 ⊆ ∪ 𝑆 ↔ ¬ ∪ 𝑆 ∈ 𝑏 ) )
16 12 14 15 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ Fin ) ∧ 𝑏 ∈ ω ) → ( 𝑏 ⊆ ∪ 𝑆 ↔ ¬ ∪ 𝑆 ∈ 𝑏 ) )
17 11 16 syl5ib ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ Fin ) ∧ 𝑏 ∈ ω ) → ( 𝑏 ∈ 𝑆 → ¬ ∪ 𝑆 ∈ 𝑏 ) )
18 17 con2d ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ Fin ) ∧ 𝑏 ∈ ω ) → ( ∪ 𝑆 ∈ 𝑏 → ¬ 𝑏 ∈ 𝑆 ) )
19 18 impr ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ Fin ) ∧ ( 𝑏 ∈ ω ∧ ∪ 𝑆 ∈ 𝑏 ) ) → ¬ 𝑏 ∈ 𝑆 )
20 4 eleq2i ⊢ ( 𝑏 ∈ 𝑆 ↔ 𝑏 ∈ { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹 ‘ 𝑦 ) } )
21 19 20 sylnib ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ Fin ) ∧ ( 𝑏 ∈ ω ∧ ∪ 𝑆 ∈ 𝑏 ) ) → ¬ 𝑏 ∈ { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹 ‘ 𝑦 ) } )
22 suceq ⊢ ( 𝑦 = 𝑏 → suc 𝑦 = suc 𝑏 )
23 22 fveq2d ⊢ ( 𝑦 = 𝑏 → ( 𝐹 ‘ suc 𝑦 ) = ( 𝐹 ‘ suc 𝑏 ) )
24 fveq2 ⊢ ( 𝑦 = 𝑏 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑏 ) )
25 23 24 psseq12d ⊢ ( 𝑦 = 𝑏 → ( ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) )
26 25 elrab3 ⊢ ( 𝑏 ∈ ω → ( 𝑏 ∈ { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹 ‘ 𝑦 ) } ↔ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) )
27 26 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ Fin ) ∧ ( 𝑏 ∈ ω ∧ ∪ 𝑆 ∈ 𝑏 ) ) → ( 𝑏 ∈ { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹 ‘ 𝑦 ) } ↔ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) )
28 21 27 mtbid ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ Fin ) ∧ ( 𝑏 ∈ ω ∧ ∪ 𝑆 ∈ 𝑏 ) ) → ¬ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) )
29 28 expr ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ Fin ) ∧ 𝑏 ∈ ω ) → ( ∪ 𝑆 ∈ 𝑏 → ¬ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) )
30 imnan ⊢ ( ( ∪ 𝑆 ∈ 𝑏 → ¬ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) ↔ ¬ ( ∪ 𝑆 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) )
31 29 30 sylib ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ Fin ) ∧ 𝑏 ∈ ω ) → ¬ ( ∪ 𝑆 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) )
32 31 nrexdv ⊢ ( ( 𝜑 ∧ 𝑆 ∈ Fin ) → ¬ ∃ 𝑏 ∈ ω ( ∪ 𝑆 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) )
33 eleq1 ⊢ ( 𝑎 = ∪ 𝑆 → ( 𝑎 ∈ 𝑏 ↔ ∪ 𝑆 ∈ 𝑏 ) )
34 33 anbi1d ⊢ ( 𝑎 = ∪ 𝑆 → ( ( 𝑎 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) ↔ ( ∪ 𝑆 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) ) )
35 34 rexbidv ⊢ ( 𝑎 = ∪ 𝑆 → ( ∃ 𝑏 ∈ ω ( 𝑎 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) ↔ ∃ 𝑏 ∈ ω ( ∪ 𝑆 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) ) )
36 35 notbid ⊢ ( 𝑎 = ∪ 𝑆 → ( ¬ ∃ 𝑏 ∈ ω ( 𝑎 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) ↔ ¬ ∃ 𝑏 ∈ ω ( ∪ 𝑆 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) ) )
37 36 rspcev ⊢ ( ( ∪ 𝑆 ∈ ω ∧ ¬ ∃ 𝑏 ∈ ω ( ∪ 𝑆 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) ) → ∃ 𝑎 ∈ ω ¬ ∃ 𝑏 ∈ ω ( 𝑎 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) )
38 10 32 37 syl2anc ⊢ ( ( 𝜑 ∧ 𝑆 ∈ Fin ) → ∃ 𝑎 ∈ ω ¬ ∃ 𝑏 ∈ ω ( 𝑎 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) )
39 rexnal ⊢ ( ∃ 𝑎 ∈ ω ¬ ∃ 𝑏 ∈ ω ( 𝑎 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) ↔ ¬ ∀ 𝑎 ∈ ω ∃ 𝑏 ∈ ω ( 𝑎 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) )
40 38 39 sylib ⊢ ( ( 𝜑 ∧ 𝑆 ∈ Fin ) → ¬ ∀ 𝑎 ∈ ω ∃ 𝑏 ∈ ω ( 𝑎 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) )
41 40 ex ⊢ ( 𝜑 → ( 𝑆 ∈ Fin → ¬ ∀ 𝑎 ∈ ω ∃ 𝑏 ∈ ω ( 𝑎 ∈ 𝑏 ∧ ( 𝐹 ‘ suc 𝑏 ) ⊊ ( 𝐹 ‘ 𝑏 ) ) ) )
42 6 41 mt2d ⊢ ( 𝜑 → ¬ 𝑆 ∈ Fin )