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

Metamath Proof Explorer

Theorem isf32lem11

Description: Lemma for isfin3-2 . Remove hypotheses from isf32lem10 . (Contributed by Stefan O'Rear, 17-May-2015)

Ref Expression
Assertion isf32lem11 ( ( 𝐺 ∈ 𝑉 ∧ ( 𝐹 : ω ⟶ 𝒫 𝐺 ∧ ∀ 𝑏 ∈ ω ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) ∧ ¬ ∩ ran 𝐹 ∈ ran 𝐹 ) ) → ω ≼* 𝐺 )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐹 : ω ⟶ 𝒫 𝐺 ∧ ∀ 𝑏 ∈ ω ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) ∧ ¬ ∩ ran 𝐹 ∈ ran 𝐹 ) → 𝐹 : ω ⟶ 𝒫 𝐺 )
2 suceq ⊢ ( 𝑏 = 𝑐 → suc 𝑏 = suc 𝑐 )
3 2 fveq2d ⊢ ( 𝑏 = 𝑐 → ( 𝐹 ‘ suc 𝑏 ) = ( 𝐹 ‘ suc 𝑐 ) )
4 fveq2 ⊢ ( 𝑏 = 𝑐 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑐 ) )
5 3 4 sseq12d ⊢ ( 𝑏 = 𝑐 → ( ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ suc 𝑐 ) ⊆ ( 𝐹 ‘ 𝑐 ) ) )
6 5 cbvralvw ⊢ ( ∀ 𝑏 ∈ ω ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) ↔ ∀ 𝑐 ∈ ω ( 𝐹 ‘ suc 𝑐 ) ⊆ ( 𝐹 ‘ 𝑐 ) )
7 6 biimpi ⊢ ( ∀ 𝑏 ∈ ω ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) → ∀ 𝑐 ∈ ω ( 𝐹 ‘ suc 𝑐 ) ⊆ ( 𝐹 ‘ 𝑐 ) )
8 7 3ad2ant2 ⊢ ( ( 𝐹 : ω ⟶ 𝒫 𝐺 ∧ ∀ 𝑏 ∈ ω ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) ∧ ¬ ∩ ran 𝐹 ∈ ran 𝐹 ) → ∀ 𝑐 ∈ ω ( 𝐹 ‘ suc 𝑐 ) ⊆ ( 𝐹 ‘ 𝑐 ) )
9 simp3 ⊢ ( ( 𝐹 : ω ⟶ 𝒫 𝐺 ∧ ∀ 𝑏 ∈ ω ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) ∧ ¬ ∩ ran 𝐹 ∈ ran 𝐹 ) → ¬ ∩ ran 𝐹 ∈ ran 𝐹 )
10 suceq ⊢ ( 𝑒 = 𝑑 → suc 𝑒 = suc 𝑑 )
11 10 fveq2d ⊢ ( 𝑒 = 𝑑 → ( 𝐹 ‘ suc 𝑒 ) = ( 𝐹 ‘ suc 𝑑 ) )
12 fveq2 ⊢ ( 𝑒 = 𝑑 → ( 𝐹 ‘ 𝑒 ) = ( 𝐹 ‘ 𝑑 ) )
13 11 12 psseq12d ⊢ ( 𝑒 = 𝑑 → ( ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) ↔ ( 𝐹 ‘ suc 𝑑 ) ⊊ ( 𝐹 ‘ 𝑑 ) ) )
14 13 cbvrabv ⊢ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } = { 𝑑 ∈ ω ∣ ( 𝐹 ‘ suc 𝑑 ) ⊊ ( 𝐹 ‘ 𝑑 ) }
15 eqid ⊢ ( 𝑓 ∈ ω ↦ ( ℩ 𝑔 ∈ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ( 𝑔 ∩ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ) ≈ 𝑓 ) ) = ( 𝑓 ∈ ω ↦ ( ℩ 𝑔 ∈ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ( 𝑔 ∩ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ) ≈ 𝑓 ) )
16 eqid ⊢ ( ( ℎ ∈ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ↦ ( ( 𝐹 ‘ ℎ ) ∖ ( 𝐹 ‘ suc ℎ ) ) ) ∘ ( 𝑓 ∈ ω ↦ ( ℩ 𝑔 ∈ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ( 𝑔 ∩ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ) ≈ 𝑓 ) ) ) = ( ( ℎ ∈ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ↦ ( ( 𝐹 ‘ ℎ ) ∖ ( 𝐹 ‘ suc ℎ ) ) ) ∘ ( 𝑓 ∈ ω ↦ ( ℩ 𝑔 ∈ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ( 𝑔 ∩ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ) ≈ 𝑓 ) ) )
17 eqid ⊢ ( 𝑘 ∈ 𝐺 ↦ ( ℩ 𝑙 ( 𝑙 ∈ ω ∧ 𝑘 ∈ ( ( ( ℎ ∈ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ↦ ( ( 𝐹 ‘ ℎ ) ∖ ( 𝐹 ‘ suc ℎ ) ) ) ∘ ( 𝑓 ∈ ω ↦ ( ℩ 𝑔 ∈ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ( 𝑔 ∩ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ) ≈ 𝑓 ) ) ) ‘ 𝑙 ) ) ) ) = ( 𝑘 ∈ 𝐺 ↦ ( ℩ 𝑙 ( 𝑙 ∈ ω ∧ 𝑘 ∈ ( ( ( ℎ ∈ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ↦ ( ( 𝐹 ‘ ℎ ) ∖ ( 𝐹 ‘ suc ℎ ) ) ) ∘ ( 𝑓 ∈ ω ↦ ( ℩ 𝑔 ∈ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ( 𝑔 ∩ { 𝑒 ∈ ω ∣ ( 𝐹 ‘ suc 𝑒 ) ⊊ ( 𝐹 ‘ 𝑒 ) } ) ≈ 𝑓 ) ) ) ‘ 𝑙 ) ) ) )
18 1 8 9 14 15 16 17 isf32lem10 ⊢ ( ( 𝐹 : ω ⟶ 𝒫 𝐺 ∧ ∀ 𝑏 ∈ ω ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) ∧ ¬ ∩ ran 𝐹 ∈ ran 𝐹 ) → ( 𝐺 ∈ 𝑉 → ω ≼* 𝐺 ) )
19 18 impcom ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝐹 : ω ⟶ 𝒫 𝐺 ∧ ∀ 𝑏 ∈ ω ( 𝐹 ‘ suc 𝑏 ) ⊆ ( 𝐹 ‘ 𝑏 ) ∧ ¬ ∩ ran 𝐹 ∈ ran 𝐹 ) ) → ω ≼* 𝐺 )