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 ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
Assertion fin23lem41 ⊢ A ∈ F → A ∈ FinIII

Proof

Step Hyp Ref Expression
1 fin23lem40.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
2 brdomi ⊢ ω ≼ 𝒫 A → ∃ b b : ω ⟶ 1-1 𝒫 A
3 1 fin23lem33 ⊢ A ∈ F → ∃ c ∀ d d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ d ⊆ A → c ⁡ d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ c ⁡ d ⊂ ⋃ ran ⁡ d
4 3 adantl ⊢ b : ω ⟶ 1-1 𝒫 A ∧ A ∈ F → ∃ c ∀ d d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ d ⊆ A → c ⁡ d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ c ⁡ d ⊂ ⋃ ran ⁡ d
5 ssv ⊢ 𝒫 A ⊆ V
6 f1ss ⊢ b : ω ⟶ 1-1 𝒫 A ∧ 𝒫 A ⊆ V → b : ω ⟶ 1-1 V
7 5 6 mpan2 ⊢ b : ω ⟶ 1-1 𝒫 A → b : ω ⟶ 1-1 V
8 7 ad2antrr ⊢ b : ω ⟶ 1-1 𝒫 A ∧ A ∈ F ∧ ∀ d d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ d ⊆ A → c ⁡ d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ c ⁡ d ⊂ ⋃ ran ⁡ d → b : ω ⟶ 1-1 V
9 f1f ⊢ b : ω ⟶ 1-1 𝒫 A → b : ω ⟶ 𝒫 A
10 frn ⊢ b : ω ⟶ 𝒫 A → ran ⁡ b ⊆ 𝒫 A
11 uniss ⊢ ran ⁡ b ⊆ 𝒫 A → ⋃ ran ⁡ b ⊆ ⋃ 𝒫 A
12 9 10 11 3syl ⊢ b : ω ⟶ 1-1 𝒫 A → ⋃ ran ⁡ b ⊆ ⋃ 𝒫 A
13 unipw ⊢ ⋃ 𝒫 A = A
14 12 13 sseqtrdi ⊢ b : ω ⟶ 1-1 𝒫 A → ⋃ ran ⁡ b ⊆ A
15 14 ad2antrr ⊢ b : ω ⟶ 1-1 𝒫 A ∧ A ∈ F ∧ ∀ d d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ d ⊆ A → c ⁡ d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ c ⁡ d ⊂ ⋃ ran ⁡ d → ⋃ ran ⁡ b ⊆ A
16 f1eq1 ⊢ d = e → d : ω ⟶ 1-1 V ↔ e : ω ⟶ 1-1 V
17 rneq ⊢ d = e → ran ⁡ d = ran ⁡ e
18 17 unieqd ⊢ d = e → ⋃ ran ⁡ d = ⋃ ran ⁡ e
19 18 sseq1d ⊢ d = e → ⋃ ran ⁡ d ⊆ A ↔ ⋃ ran ⁡ e ⊆ A
20 16 19 anbi12d ⊢ d = e → d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ d ⊆ A ↔ e : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ e ⊆ A
21 fveq2 ⊢ d = e → c ⁡ d = c ⁡ e
22 f1eq1 ⊢ c ⁡ d = c ⁡ e → c ⁡ d : ω ⟶ 1-1 V ↔ c ⁡ e : ω ⟶ 1-1 V
23 21 22 syl ⊢ d = e → c ⁡ d : ω ⟶ 1-1 V ↔ c ⁡ e : ω ⟶ 1-1 V
24 21 rneqd ⊢ d = e → ran ⁡ c ⁡ d = ran ⁡ c ⁡ e
25 24 unieqd ⊢ d = e → ⋃ ran ⁡ c ⁡ d = ⋃ ran ⁡ c ⁡ e
26 25 18 psseq12d ⊢ d = e → ⋃ ran ⁡ c ⁡ d ⊂ ⋃ ran ⁡ d ↔ ⋃ ran ⁡ c ⁡ e ⊂ ⋃ ran ⁡ e
27 23 26 anbi12d ⊢ d = e → c ⁡ d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ c ⁡ d ⊂ ⋃ ran ⁡ d ↔ c ⁡ e : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ c ⁡ e ⊂ ⋃ ran ⁡ e
28 20 27 imbi12d ⊢ d = e → d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ d ⊆ A → c ⁡ d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ c ⁡ d ⊂ ⋃ ran ⁡ d ↔ e : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ e ⊆ A → c ⁡ e : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ c ⁡ e ⊂ ⋃ ran ⁡ e
29 28 cbvalvw ⊢ ∀ d d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ d ⊆ A → c ⁡ d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ c ⁡ d ⊂ ⋃ ran ⁡ d ↔ ∀ e e : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ e ⊆ A → c ⁡ e : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ c ⁡ e ⊂ ⋃ ran ⁡ e
30 29 bilani ⊢ b : ω ⟶ 1-1 𝒫 A ∧ A ∈ F ∧ ∀ d d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ d ⊆ A → c ⁡ d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ c ⁡ d ⊂ ⋃ ran ⁡ d → ∀ e e : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ e ⊆ A → c ⁡ e : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ c ⁡ e ⊂ ⋃ ran ⁡ e
31 eqid ⊢ rec ⁡ c b ↾ ω = rec ⁡ c b ↾ ω
32 1 8 15 30 31 fin23lem39 ⊢ b : ω ⟶ 1-1 𝒫 A ∧ A ∈ F ∧ ∀ d d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ d ⊆ A → c ⁡ d : ω ⟶ 1-1 V ∧ ⋃ ran ⁡ c ⁡ d ⊂ ⋃ ran ⁡ d → ¬ A ∈ F
33 4 32 exlimddv ⊢ b : ω ⟶ 1-1 𝒫 A ∧ A ∈ F → ¬ A ∈ F
34 33 pm2.01da ⊢ b : ω ⟶ 1-1 𝒫 A → ¬ A ∈ F
35 34 exlimiv ⊢ ∃ b b : ω ⟶ 1-1 𝒫 A → ¬ A ∈ F
36 2 35 syl ⊢ ω ≼ 𝒫 A → ¬ A ∈ F
37 36 con2i ⊢ A ∈ F → ¬ ω ≼ 𝒫 A
38 pwexg ⊢ A ∈ F → 𝒫 A ∈ V
39 isfin4-2 ⊢ 𝒫 A ∈ V → 𝒫 A ∈ FinIV ↔ ¬ ω ≼ 𝒫 A
40 38 39 syl ⊢ A ∈ F → 𝒫 A ∈ FinIV ↔ ¬ ω ≼ 𝒫 A
41 37 40 mpbird ⊢ A ∈ F → 𝒫 A ∈ FinIV
42 isfin3 ⊢ A ∈ FinIII ↔ 𝒫 A ∈ FinIV
43 41 42 sylibr ⊢ A ∈ F → A ∈ FinIII