Theorem isf33lem

Description: Lemma for isfin3-3 . (Contributed by Stefan O'Rear, 17-May-2015)

	Ref	Expression
Assertion	isf33lem	⊢ FinIII = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }

Proof

Step	Hyp	Ref	Expression
1		isfin32i	⊢ ( 𝑓 ∈ FinIII → ¬ ω ≼* 𝑓 )
2		fveq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 ‘ suc 𝑥 ) = ( 𝑏 ‘ suc 𝑥 ) )
3		fveq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) )
4	2 3	sseq12d	⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) ↔ ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) ) )
5	4	ralbidv	⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) ) )
6		rneq	⊢ ( 𝑎 = 𝑏 → ran 𝑎 = ran 𝑏 )
7	6	inteqd	⊢ ( 𝑎 = 𝑏 → ∩ ran 𝑎 = ∩ ran 𝑏 )
8	7 6	eleq12d	⊢ ( 𝑎 = 𝑏 → ( ∩ ran 𝑎 ∈ ran 𝑎 ↔ ∩ ran 𝑏 ∈ ran 𝑏 ) )
9	5 8	imbi12d	⊢ ( 𝑎 = 𝑏 → ( ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) ↔ ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ) )
10	9	cbvralvw	⊢ ( ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) )
11		pweq	⊢ ( 𝑔 = 𝑦 → 𝒫 𝑔 = 𝒫 𝑦 )
12	11	oveq1d	⊢ ( 𝑔 = 𝑦 → ( 𝒫 𝑔 ↑m ω ) = ( 𝒫 𝑦 ↑m ω ) )
13	12	raleqdv	⊢ ( 𝑔 = 𝑦 → ( ∀ 𝑏 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝑦 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ) )
14	10 13	bitrid	⊢ ( 𝑔 = 𝑦 → ( ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝑦 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ) )
15	14	cbvabv	⊢ { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } = { 𝑦 ∣ ∀ 𝑏 ∈ ( 𝒫 𝑦 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) }
16	15	isf32lem12	⊢ ( 𝑓 ∈ FinIII → ( ¬ ω ≼* 𝑓 → 𝑓 ∈ { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } ) )
17	1 16	mpd	⊢ ( 𝑓 ∈ FinIII → 𝑓 ∈ { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } )
18	10	abbii	⊢ { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } = { 𝑔 ∣ ∀ 𝑏 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) }
19	18	fin23lem41	⊢ ( 𝑓 ∈ { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } → 𝑓 ∈ FinIII )
20	17 19	impbii	⊢ ( 𝑓 ∈ FinIII ↔ 𝑓 ∈ { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } )
21	20	eqriv	⊢ FinIII = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }