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

Metamath Proof Explorer

Theorem isf32lem6

Description: Lemma for isfin3-2 . Each K value is nonempty. (Contributed by Stefan O'Rear, 5-Nov-2014)

Ref Expression
Hypotheses isf32lem.a ⊢ ( 𝜑 → 𝐹 : ω ⟶ 𝒫 𝐺 )
isf32lem.b ⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
isf32lem.c ⊢ ( 𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹 )
isf32lem.d ⊢ 𝑆 = { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹 ‘ 𝑦 ) }
isf32lem.e ⊢ 𝐽 = ( 𝑢 ∈ ω ↦ ( ℩ 𝑣 ∈ 𝑆 ( 𝑣 ∩ 𝑆 ) ≈ 𝑢 ) )
isf32lem.f ⊢ 𝐾 = ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 )
Assertion isf32lem6 ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐾 ‘ 𝐴 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 isf32lem.a ⊢ ( 𝜑 → 𝐹 : ω ⟶ 𝒫 𝐺 )
2 isf32lem.b ⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
3 isf32lem.c ⊢ ( 𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹 )
4 isf32lem.d ⊢ 𝑆 = { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹 ‘ 𝑦 ) }
5 isf32lem.e ⊢ 𝐽 = ( 𝑢 ∈ ω ↦ ( ℩ 𝑣 ∈ 𝑆 ( 𝑣 ∩ 𝑆 ) ≈ 𝑢 ) )
6 isf32lem.f ⊢ 𝐾 = ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 )
7 6 fveq1i ⊢ ( 𝐾 ‘ 𝐴 ) = ( ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐴 )
8 4 ssrab3 ⊢ 𝑆 ⊆ ω
9 1 2 3 4 isf32lem5 ⊢ ( 𝜑 → ¬ 𝑆 ∈ Fin )
10 5 fin23lem22 ⊢ ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) → 𝐽 : ω –1-1-onto→ 𝑆 )
11 8 9 10 sylancr ⊢ ( 𝜑 → 𝐽 : ω –1-1-onto→ 𝑆 )
12 f1of ⊢ ( 𝐽 : ω –1-1-onto→ 𝑆 → 𝐽 : ω ⟶ 𝑆 )
13 11 12 syl ⊢ ( 𝜑 → 𝐽 : ω ⟶ 𝑆 )
14 fvco3 ⊢ ( ( 𝐽 : ω ⟶ 𝑆 ∧ 𝐴 ∈ ω ) → ( ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐴 ) = ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽 ‘ 𝐴 ) ) )
15 13 14 sylan ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐴 ) = ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽 ‘ 𝐴 ) ) )
16 9 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ¬ 𝑆 ∈ Fin )
17 8 16 10 sylancr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → 𝐽 : ω –1-1-onto→ 𝑆 )
18 17 12 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → 𝐽 : ω ⟶ 𝑆 )
19 ffvelcdm ⊢ ( ( 𝐽 : ω ⟶ 𝑆 ∧ 𝐴 ∈ ω ) → ( 𝐽 ‘ 𝐴 ) ∈ 𝑆 )
20 18 19 sylancom ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐽 ‘ 𝐴 ) ∈ 𝑆 )
21 fveq2 ⊢ ( 𝑤 = ( 𝐽 ‘ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) )
22 suceq ⊢ ( 𝑤 = ( 𝐽 ‘ 𝐴 ) → suc 𝑤 = suc ( 𝐽 ‘ 𝐴 ) )
23 22 fveq2d ⊢ ( 𝑤 = ( 𝐽 ‘ 𝐴 ) → ( 𝐹 ‘ suc 𝑤 ) = ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) )
24 21 23 difeq12d ⊢ ( 𝑤 = ( 𝐽 ‘ 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) = ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ) )
25 eqid ⊢ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) = ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) )
26 fvex ⊢ ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∈ V
27 26 difexi ⊢ ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ) ∈ V
28 24 25 27 fvmpt ⊢ ( ( 𝐽 ‘ 𝐴 ) ∈ 𝑆 → ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽 ‘ 𝐴 ) ) = ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ) )
29 20 28 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽 ‘ 𝐴 ) ) = ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ) )
30 15 29 eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐴 ) = ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ) )
31 7 30 eqtrid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐾 ‘ 𝐴 ) = ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ) )
32 suceq ⊢ ( 𝑦 = ( 𝐽 ‘ 𝐴 ) → suc 𝑦 = suc ( 𝐽 ‘ 𝐴 ) )
33 32 fveq2d ⊢ ( 𝑦 = ( 𝐽 ‘ 𝐴 ) → ( 𝐹 ‘ suc 𝑦 ) = ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) )
34 fveq2 ⊢ ( 𝑦 = ( 𝐽 ‘ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) )
35 33 34 psseq12d ⊢ ( 𝑦 = ( 𝐽 ‘ 𝐴 ) → ( ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ⊊ ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ) )
36 35 4 elrab2 ⊢ ( ( 𝐽 ‘ 𝐴 ) ∈ 𝑆 ↔ ( ( 𝐽 ‘ 𝐴 ) ∈ ω ∧ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ⊊ ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ) )
37 36 simprbi ⊢ ( ( 𝐽 ‘ 𝐴 ) ∈ 𝑆 → ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ⊊ ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) )
38 20 37 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ⊊ ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) )
39 df-pss ⊢ ( ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ⊊ ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ↔ ( ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ⊆ ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∧ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ≠ ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ) )
40 38 39 sylib ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ⊆ ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∧ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ≠ ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ) )
41 pssdifn0 ⊢ ( ( ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ⊆ ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∧ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ≠ ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ) → ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ) ≠ ∅ )
42 40 41 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ) ≠ ∅ )
43 31 42 eqnetrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐾 ‘ 𝐴 ) ≠ ∅ )