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 𝐹 ) ) → ω ≼* 𝐺 )