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

Metamath Proof Explorer

Theorem fin23lem41

Description: Lemma for fin23 . A set which satisfies the descending sequence condition must be III-finite. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypothesis fin23lem40.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
Assertion fin23lem41 ( 𝐴 ∈ 𝐹 → 𝐴 ∈ FinIII )

Proof

Step Hyp Ref Expression
1 fin23lem40.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
2 brdomi ⊢ ( ω ≼ 𝒫 𝐴 → ∃ 𝑏 𝑏 : ω –1-1→ 𝒫 𝐴 )
3 1 fin23lem33 ⊢ ( 𝐴 ∈ 𝐹 → ∃ 𝑐 ∀ 𝑑 ( ( 𝑑 : ω –1-1→ V ∧ ∪ ran 𝑑 ⊆ 𝐴 ) → ( ( 𝑐 ‘ 𝑑 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑑 ) ⊊ ∪ ran 𝑑 ) ) )
4 3 adantl ⊢ ( ( 𝑏 : ω –1-1→ 𝒫 𝐴 ∧ 𝐴 ∈ 𝐹 ) → ∃ 𝑐 ∀ 𝑑 ( ( 𝑑 : ω –1-1→ V ∧ ∪ ran 𝑑 ⊆ 𝐴 ) → ( ( 𝑐 ‘ 𝑑 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑑 ) ⊊ ∪ ran 𝑑 ) ) )
5 ssv ⊢ 𝒫 𝐴 ⊆ V
6 f1ss ⊢ ( ( 𝑏 : ω –1-1→ 𝒫 𝐴 ∧ 𝒫 𝐴 ⊆ V ) → 𝑏 : ω –1-1→ V )
7 5 6 mpan2 ⊢ ( 𝑏 : ω –1-1→ 𝒫 𝐴 → 𝑏 : ω –1-1→ V )
8 7 ad2antrr ⊢ ( ( ( 𝑏 : ω –1-1→ 𝒫 𝐴 ∧ 𝐴 ∈ 𝐹 ) ∧ ∀ 𝑑 ( ( 𝑑 : ω –1-1→ V ∧ ∪ ran 𝑑 ⊆ 𝐴 ) → ( ( 𝑐 ‘ 𝑑 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑑 ) ⊊ ∪ ran 𝑑 ) ) ) → 𝑏 : ω –1-1→ V )
9 f1f ⊢ ( 𝑏 : ω –1-1→ 𝒫 𝐴 → 𝑏 : ω ⟶ 𝒫 𝐴 )
10 frn ⊢ ( 𝑏 : ω ⟶ 𝒫 𝐴 → ran 𝑏 ⊆ 𝒫 𝐴 )
11 uniss ⊢ ( ran 𝑏 ⊆ 𝒫 𝐴 → ∪ ran 𝑏 ⊆ ∪ 𝒫 𝐴 )
12 9 10 11 3syl ⊢ ( 𝑏 : ω –1-1→ 𝒫 𝐴 → ∪ ran 𝑏 ⊆ ∪ 𝒫 𝐴 )
13 unipw ⊢ ∪ 𝒫 𝐴 = 𝐴
14 12 13 sseqtrdi ⊢ ( 𝑏 : ω –1-1→ 𝒫 𝐴 → ∪ ran 𝑏 ⊆ 𝐴 )
15 14 ad2antrr ⊢ ( ( ( 𝑏 : ω –1-1→ 𝒫 𝐴 ∧ 𝐴 ∈ 𝐹 ) ∧ ∀ 𝑑 ( ( 𝑑 : ω –1-1→ V ∧ ∪ ran 𝑑 ⊆ 𝐴 ) → ( ( 𝑐 ‘ 𝑑 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑑 ) ⊊ ∪ ran 𝑑 ) ) ) → ∪ ran 𝑏 ⊆ 𝐴 )
16 f1eq1 ⊢ ( 𝑑 = 𝑒 → ( 𝑑 : ω –1-1→ V ↔ 𝑒 : ω –1-1→ V ) )
17 rneq ⊢ ( 𝑑 = 𝑒 → ran 𝑑 = ran 𝑒 )
18 17 unieqd ⊢ ( 𝑑 = 𝑒 → ∪ ran 𝑑 = ∪ ran 𝑒 )
19 18 sseq1d ⊢ ( 𝑑 = 𝑒 → ( ∪ ran 𝑑 ⊆ 𝐴 ↔ ∪ ran 𝑒 ⊆ 𝐴 ) )
20 16 19 anbi12d ⊢ ( 𝑑 = 𝑒 → ( ( 𝑑 : ω –1-1→ V ∧ ∪ ran 𝑑 ⊆ 𝐴 ) ↔ ( 𝑒 : ω –1-1→ V ∧ ∪ ran 𝑒 ⊆ 𝐴 ) ) )
21 fveq2 ⊢ ( 𝑑 = 𝑒 → ( 𝑐 ‘ 𝑑 ) = ( 𝑐 ‘ 𝑒 ) )
22 f1eq1 ⊢ ( ( 𝑐 ‘ 𝑑 ) = ( 𝑐 ‘ 𝑒 ) → ( ( 𝑐 ‘ 𝑑 ) : ω –1-1→ V ↔ ( 𝑐 ‘ 𝑒 ) : ω –1-1→ V ) )
23 21 22 syl ⊢ ( 𝑑 = 𝑒 → ( ( 𝑐 ‘ 𝑑 ) : ω –1-1→ V ↔ ( 𝑐 ‘ 𝑒 ) : ω –1-1→ V ) )
24 21 rneqd ⊢ ( 𝑑 = 𝑒 → ran ( 𝑐 ‘ 𝑑 ) = ran ( 𝑐 ‘ 𝑒 ) )
25 24 unieqd ⊢ ( 𝑑 = 𝑒 → ∪ ran ( 𝑐 ‘ 𝑑 ) = ∪ ran ( 𝑐 ‘ 𝑒 ) )
26 25 18 psseq12d ⊢ ( 𝑑 = 𝑒 → ( ∪ ran ( 𝑐 ‘ 𝑑 ) ⊊ ∪ ran 𝑑 ↔ ∪ ran ( 𝑐 ‘ 𝑒 ) ⊊ ∪ ran 𝑒 ) )
27 23 26 anbi12d ⊢ ( 𝑑 = 𝑒 → ( ( ( 𝑐 ‘ 𝑑 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑑 ) ⊊ ∪ ran 𝑑 ) ↔ ( ( 𝑐 ‘ 𝑒 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑒 ) ⊊ ∪ ran 𝑒 ) ) )
28 20 27 imbi12d ⊢ ( 𝑑 = 𝑒 → ( ( ( 𝑑 : ω –1-1→ V ∧ ∪ ran 𝑑 ⊆ 𝐴 ) → ( ( 𝑐 ‘ 𝑑 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑑 ) ⊊ ∪ ran 𝑑 ) ) ↔ ( ( 𝑒 : ω –1-1→ V ∧ ∪ ran 𝑒 ⊆ 𝐴 ) → ( ( 𝑐 ‘ 𝑒 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑒 ) ⊊ ∪ ran 𝑒 ) ) ) )
29 28 cbvalvw ⊢ ( ∀ 𝑑 ( ( 𝑑 : ω –1-1→ V ∧ ∪ ran 𝑑 ⊆ 𝐴 ) → ( ( 𝑐 ‘ 𝑑 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑑 ) ⊊ ∪ ran 𝑑 ) ) ↔ ∀ 𝑒 ( ( 𝑒 : ω –1-1→ V ∧ ∪ ran 𝑒 ⊆ 𝐴 ) → ( ( 𝑐 ‘ 𝑒 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑒 ) ⊊ ∪ ran 𝑒 ) ) )
30 29 biimpi ⊢ ( ∀ 𝑑 ( ( 𝑑 : ω –1-1→ V ∧ ∪ ran 𝑑 ⊆ 𝐴 ) → ( ( 𝑐 ‘ 𝑑 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑑 ) ⊊ ∪ ran 𝑑 ) ) → ∀ 𝑒 ( ( 𝑒 : ω –1-1→ V ∧ ∪ ran 𝑒 ⊆ 𝐴 ) → ( ( 𝑐 ‘ 𝑒 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑒 ) ⊊ ∪ ran 𝑒 ) ) )
31 30 adantl ⊢ ( ( ( 𝑏 : ω –1-1→ 𝒫 𝐴 ∧ 𝐴 ∈ 𝐹 ) ∧ ∀ 𝑑 ( ( 𝑑 : ω –1-1→ V ∧ ∪ ran 𝑑 ⊆ 𝐴 ) → ( ( 𝑐 ‘ 𝑑 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑑 ) ⊊ ∪ ran 𝑑 ) ) ) → ∀ 𝑒 ( ( 𝑒 : ω –1-1→ V ∧ ∪ ran 𝑒 ⊆ 𝐴 ) → ( ( 𝑐 ‘ 𝑒 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑒 ) ⊊ ∪ ran 𝑒 ) ) )
32 eqid ⊢ ( rec ( 𝑐 , 𝑏 ) ↾ ω ) = ( rec ( 𝑐 , 𝑏 ) ↾ ω )
33 1 8 15 31 32 fin23lem39 ⊢ ( ( ( 𝑏 : ω –1-1→ 𝒫 𝐴 ∧ 𝐴 ∈ 𝐹 ) ∧ ∀ 𝑑 ( ( 𝑑 : ω –1-1→ V ∧ ∪ ran 𝑑 ⊆ 𝐴 ) → ( ( 𝑐 ‘ 𝑑 ) : ω –1-1→ V ∧ ∪ ran ( 𝑐 ‘ 𝑑 ) ⊊ ∪ ran 𝑑 ) ) ) → ¬ 𝐴 ∈ 𝐹 )
34 4 33 exlimddv ⊢ ( ( 𝑏 : ω –1-1→ 𝒫 𝐴 ∧ 𝐴 ∈ 𝐹 ) → ¬ 𝐴 ∈ 𝐹 )
35 34 pm2.01da ⊢ ( 𝑏 : ω –1-1→ 𝒫 𝐴 → ¬ 𝐴 ∈ 𝐹 )
36 35 exlimiv ⊢ ( ∃ 𝑏 𝑏 : ω –1-1→ 𝒫 𝐴 → ¬ 𝐴 ∈ 𝐹 )
37 2 36 syl ⊢ ( ω ≼ 𝒫 𝐴 → ¬ 𝐴 ∈ 𝐹 )
38 37 con2i ⊢ ( 𝐴 ∈ 𝐹 → ¬ ω ≼ 𝒫 𝐴 )
39 pwexg ⊢ ( 𝐴 ∈ 𝐹 → 𝒫 𝐴 ∈ V )
40 isfin4-2 ⊢ ( 𝒫 𝐴 ∈ V → ( 𝒫 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝒫 𝐴 ) )
41 39 40 syl ⊢ ( 𝐴 ∈ 𝐹 → ( 𝒫 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝒫 𝐴 ) )
42 38 41 mpbird ⊢ ( 𝐴 ∈ 𝐹 → 𝒫 𝐴 ∈ FinIV )
43 isfin3 ⊢ ( 𝐴 ∈ FinIII ↔ 𝒫 𝐴 ∈ FinIV )
44 42 43 sylibr ⊢ ( 𝐴 ∈ 𝐹 → 𝐴 ∈ FinIII )