Metamath Proof Explorer

Theorem fin23lem40

Description: Lemma for fin23 . Fin2 sets satisfy the descending chain condition. (Contributed by Stefan O'Rear, 3-Nov-2014)

Ref Expression
Hypothesis fin23lem40.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
Assertion fin23lem40 ⊢ A ∈ FinII → A ∈ F

Proof

Step Hyp Ref Expression
1 fin23lem40.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
2 elmapi ⊢ f ∈ 𝒫 A ω → f : ω ⟶ 𝒫 A
3 simpl ⊢ A ∈ FinII ∧ f : ω ⟶ 𝒫 A ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → A ∈ FinII
4 frn ⊢ f : ω ⟶ 𝒫 A → ran ⁡ f ⊆ 𝒫 A
5 4 ad2antrl ⊢ A ∈ FinII ∧ f : ω ⟶ 𝒫 A ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → ran ⁡ f ⊆ 𝒫 A
6 fdm ⊢ f : ω ⟶ 𝒫 A → dom ⁡ f = ω
7 peano1 ⊢ ∅ ∈ ω
8 ne0i ⊢ ∅ ∈ ω → ω ≠ ∅
9 7 8 mp1i ⊢ f : ω ⟶ 𝒫 A → ω ≠ ∅
10 6 9 eqnetrd ⊢ f : ω ⟶ 𝒫 A → dom ⁡ f ≠ ∅
11 dm0rn0 ⊢ dom ⁡ f = ∅ ↔ ran ⁡ f = ∅
12 11 necon3bii ⊢ dom ⁡ f ≠ ∅ ↔ ran ⁡ f ≠ ∅
13 10 12 sylib ⊢ f : ω ⟶ 𝒫 A → ran ⁡ f ≠ ∅
14 13 ad2antrl ⊢ A ∈ FinII ∧ f : ω ⟶ 𝒫 A ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → ran ⁡ f ≠ ∅
15 ffn ⊢ f : ω ⟶ 𝒫 A → f Fn ω
16 15 ad2antrl ⊢ A ∈ FinII ∧ f : ω ⟶ 𝒫 A ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → f Fn ω
17 sspss ⊢ f ⁡ suc ⁡ b ⊆ f ⁡ b ↔ f ⁡ suc ⁡ b ⊂ f ⁡ b ∨ f ⁡ suc ⁡ b = f ⁡ b
18 fvex ⊢ f ⁡ b ∈ V
19 fvex ⊢ f ⁡ suc ⁡ b ∈ V
20 18 19 brcnv ⊢ f ⁡ b [⊂] -1 f ⁡ suc ⁡ b ↔ f ⁡ suc ⁡ b [⊂] f ⁡ b
21 18 brrpss ⊢ f ⁡ suc ⁡ b [⊂] f ⁡ b ↔ f ⁡ suc ⁡ b ⊂ f ⁡ b
22 20 21 bitri ⊢ f ⁡ b [⊂] -1 f ⁡ suc ⁡ b ↔ f ⁡ suc ⁡ b ⊂ f ⁡ b
23 eqcom ⊢ f ⁡ b = f ⁡ suc ⁡ b ↔ f ⁡ suc ⁡ b = f ⁡ b
24 22 23 orbi12i ⊢ f ⁡ b [⊂] -1 f ⁡ suc ⁡ b ∨ f ⁡ b = f ⁡ suc ⁡ b ↔ f ⁡ suc ⁡ b ⊂ f ⁡ b ∨ f ⁡ suc ⁡ b = f ⁡ b
25 17 24 sylbb2 ⊢ f ⁡ suc ⁡ b ⊆ f ⁡ b → f ⁡ b [⊂] -1 f ⁡ suc ⁡ b ∨ f ⁡ b = f ⁡ suc ⁡ b
26 25 ralimi ⊢ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → ∀ b ∈ ω f ⁡ b [⊂] -1 f ⁡ suc ⁡ b ∨ f ⁡ b = f ⁡ suc ⁡ b
27 26 ad2antll ⊢ A ∈ FinII ∧ f : ω ⟶ 𝒫 A ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → ∀ b ∈ ω f ⁡ b [⊂] -1 f ⁡ suc ⁡ b ∨ f ⁡ b = f ⁡ suc ⁡ b
28 porpss ⊢ [⊂] Po ran ⁡ f
29 cnvpo ⊢ [⊂] Po ran ⁡ f ↔ [⊂] -1 Po ran ⁡ f
30 28 29 mpbi ⊢ [⊂] -1 Po ran ⁡ f
31 30 a1i ⊢ A ∈ FinII ∧ f : ω ⟶ 𝒫 A ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → [⊂] -1 Po ran ⁡ f
32 sornom ⊢ f Fn ω ∧ ∀ b ∈ ω f ⁡ b [⊂] -1 f ⁡ suc ⁡ b ∨ f ⁡ b = f ⁡ suc ⁡ b ∧ [⊂] -1 Po ran ⁡ f → [⊂] -1 Or ran ⁡ f
33 16 27 31 32 syl3anc ⊢ A ∈ FinII ∧ f : ω ⟶ 𝒫 A ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → [⊂] -1 Or ran ⁡ f
34 cnvso ⊢ [⊂] Or ran ⁡ f ↔ [⊂] -1 Or ran ⁡ f
35 33 34 sylibr ⊢ A ∈ FinII ∧ f : ω ⟶ 𝒫 A ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → [⊂] Or ran ⁡ f
36 fin2i2 ⊢ A ∈ FinII ∧ ran ⁡ f ⊆ 𝒫 A ∧ ran ⁡ f ≠ ∅ ∧ [⊂] Or ran ⁡ f → ⋂ ran ⁡ f ∈ ran ⁡ f
37 3 5 14 35 36 syl22anc ⊢ A ∈ FinII ∧ f : ω ⟶ 𝒫 A ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → ⋂ ran ⁡ f ∈ ran ⁡ f
38 37 expr ⊢ A ∈ FinII ∧ f : ω ⟶ 𝒫 A → ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → ⋂ ran ⁡ f ∈ ran ⁡ f
39 2 38 sylan2 ⊢ A ∈ FinII ∧ f ∈ 𝒫 A ω → ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → ⋂ ran ⁡ f ∈ ran ⁡ f
40 39 ralrimiva ⊢ A ∈ FinII → ∀ f ∈ 𝒫 A ω ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → ⋂ ran ⁡ f ∈ ran ⁡ f
41 1 isfin3ds ⊢ A ∈ FinII → A ∈ F ↔ ∀ f ∈ 𝒫 A ω ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → ⋂ ran ⁡ f ∈ ran ⁡ f
42 40 41 mpbird ⊢ A ∈ FinII → A ∈ F