Metamath Proof Explorer

Theorem fin23lem35

Description: Lemma for fin23 . Strict order property of Y . (Contributed by Stefan O'Rear, 2-Nov-2014)

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 fin23lem35 ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ∪ ran ( 𝑌 ‘ suc 𝐴 ) ⊊ ∪ 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 1 2 3 4 5 fin23lem34 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ 𝐺 ) )
7 fvex ⊢ ( 𝑌 ‘ 𝐴 ) ∈ V
8 f1eq1 ⊢ ( 𝑗 = ( 𝑌 ‘ 𝐴 ) → ( 𝑗 : ω –1-1→ V ↔ ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ) )
9 rneq ⊢ ( 𝑗 = ( 𝑌 ‘ 𝐴 ) → ran 𝑗 = ran ( 𝑌 ‘ 𝐴 ) )
10 9 unieqd ⊢ ( 𝑗 = ( 𝑌 ‘ 𝐴 ) → ∪ ran 𝑗 = ∪ ran ( 𝑌 ‘ 𝐴 ) )
11 10 sseq1d ⊢ ( 𝑗 = ( 𝑌 ‘ 𝐴 ) → ( ∪ ran 𝑗 ⊆ 𝐺 ↔ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ 𝐺 ) )
12 8 11 anbi12d ⊢ ( 𝑗 = ( 𝑌 ‘ 𝐴 ) → ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) ↔ ( ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ 𝐺 ) ) )
13 fveq2 ⊢ ( 𝑗 = ( 𝑌 ‘ 𝐴 ) → ( 𝑖 ‘ 𝑗 ) = ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) )
14 f1eq1 ⊢ ( ( 𝑖 ‘ 𝑗 ) = ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ↔ ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) : ω –1-1→ V ) )
15 13 14 syl ⊢ ( 𝑗 = ( 𝑌 ‘ 𝐴 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ↔ ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) : ω –1-1→ V ) )
16 13 rneqd ⊢ ( 𝑗 = ( 𝑌 ‘ 𝐴 ) → ran ( 𝑖 ‘ 𝑗 ) = ran ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) )
17 16 unieqd ⊢ ( 𝑗 = ( 𝑌 ‘ 𝐴 ) → ∪ ran ( 𝑖 ‘ 𝑗 ) = ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) )
18 17 10 psseq12d ⊢ ( 𝑗 = ( 𝑌 ‘ 𝐴 ) → ( ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ↔ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝐴 ) ) )
19 15 18 anbi12d ⊢ ( 𝑗 = ( 𝑌 ‘ 𝐴 ) → ( ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ↔ ( ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝐴 ) ) ) )
20 12 19 imbi12d ⊢ ( 𝑗 = ( 𝑌 ‘ 𝐴 ) → ( ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) ↔ ( ( ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ 𝐺 ) → ( ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝐴 ) ) ) ) )
21 7 20 spcv ⊢ ( ∀ 𝑗 ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) → ( ( ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ 𝐺 ) → ( ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝐴 ) ) ) )
22 4 21 syl ⊢ ( 𝜑 → ( ( ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ 𝐺 ) → ( ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝐴 ) ) ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ 𝐺 ) → ( ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝐴 ) ) ) )
24 6 23 mpd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝐴 ) ) )
25 24 simprd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝐴 ) )
26 frsuc ⊢ ( 𝐴 ∈ ω → ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ suc 𝐴 ) = ( 𝑖 ‘ ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ 𝐴 ) ) )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ suc 𝐴 ) = ( 𝑖 ‘ ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ 𝐴 ) ) )
28 5 fveq1i ⊢ ( 𝑌 ‘ suc 𝐴 ) = ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ suc 𝐴 )
29 5 fveq1i ⊢ ( 𝑌 ‘ 𝐴 ) = ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ 𝐴 )
30 29 fveq2i ⊢ ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) = ( 𝑖 ‘ ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ 𝐴 ) )
31 27 28 30 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝑌 ‘ suc 𝐴 ) = ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) )
32 31 rneqd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ran ( 𝑌 ‘ suc 𝐴 ) = ran ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) )
33 32 unieqd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ∪ ran ( 𝑌 ‘ suc 𝐴 ) = ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) )
34 33 psseq1d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ∪ ran ( 𝑌 ‘ suc 𝐴 ) ⊊ ∪ ran ( 𝑌 ‘ 𝐴 ) ↔ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝐴 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝐴 ) ) )
35 25 34 mpbird ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ∪ ran ( 𝑌 ‘ suc 𝐴 ) ⊊ ∪ ran ( 𝑌 ‘ 𝐴 ) )