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

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 ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
Assertion fin23lem40 ( 𝐴 ∈ FinII → 𝐴 ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 fin23lem40.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
2 elmapi ⊢ ( 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) → 𝑓 : ω ⟶ 𝒫 𝐴 )
3 simpl ⊢ ( ( 𝐴 ∈ FinII ∧ ( 𝑓 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ) ) → 𝐴 ∈ FinII )
4 frn ⊢ ( 𝑓 : ω ⟶ 𝒫 𝐴 → ran 𝑓 ⊆ 𝒫 𝐴 )
5 4 ad2antrl ⊢ ( ( 𝐴 ∈ FinII ∧ ( 𝑓 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ) ) → ran 𝑓 ⊆ 𝒫 𝐴 )
6 fdm ⊢ ( 𝑓 : ω ⟶ 𝒫 𝐴 → dom 𝑓 = ω )
7 peano1 ⊢ ∅ ∈ ω
8 ne0i ⊢ ( ∅ ∈ ω → ω ≠ ∅ )
9 7 8 mp1i ⊢ ( 𝑓 : ω ⟶ 𝒫 𝐴 → ω ≠ ∅ )
10 6 9 eqnetrd ⊢ ( 𝑓 : ω ⟶ 𝒫 𝐴 → dom 𝑓 ≠ ∅ )
11 dm0rn0 ⊢ ( dom 𝑓 = ∅ ↔ ran 𝑓 = ∅ )
12 11 necon3bii ⊢ ( dom 𝑓 ≠ ∅ ↔ ran 𝑓 ≠ ∅ )
13 10 12 sylib ⊢ ( 𝑓 : ω ⟶ 𝒫 𝐴 → ran 𝑓 ≠ ∅ )
14 13 ad2antrl ⊢ ( ( 𝐴 ∈ FinII ∧ ( 𝑓 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ) ) → ran 𝑓 ≠ ∅ )
15 ffn ⊢ ( 𝑓 : ω ⟶ 𝒫 𝐴 → 𝑓 Fn ω )
16 15 ad2antrl ⊢ ( ( 𝐴 ∈ FinII ∧ ( 𝑓 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ) ) → 𝑓 Fn ω )
17 sspss ⊢ ( ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ↔ ( ( 𝑓 ‘ suc 𝑏 ) ⊊ ( 𝑓 ‘ 𝑏 ) ∨ ( 𝑓 ‘ suc 𝑏 ) = ( 𝑓 ‘ 𝑏 ) ) )
18 fvex ⊢ ( 𝑓 ‘ 𝑏 ) ∈ V
19 fvex ⊢ ( 𝑓 ‘ suc 𝑏 ) ∈ V
20 18 19 brcnv ⊢ ( ( 𝑓 ‘ 𝑏 ) ◡ [⊊] ( 𝑓 ‘ suc 𝑏 ) ↔ ( 𝑓 ‘ suc 𝑏 ) [⊊] ( 𝑓 ‘ 𝑏 ) )
21 18 brrpss ⊢ ( ( 𝑓 ‘ suc 𝑏 ) [⊊] ( 𝑓 ‘ 𝑏 ) ↔ ( 𝑓 ‘ suc 𝑏 ) ⊊ ( 𝑓 ‘ 𝑏 ) )
22 20 21 bitri ⊢ ( ( 𝑓 ‘ 𝑏 ) ◡ [⊊] ( 𝑓 ‘ suc 𝑏 ) ↔ ( 𝑓 ‘ suc 𝑏 ) ⊊ ( 𝑓 ‘ 𝑏 ) )
23 eqcom ⊢ ( ( 𝑓 ‘ 𝑏 ) = ( 𝑓 ‘ suc 𝑏 ) ↔ ( 𝑓 ‘ suc 𝑏 ) = ( 𝑓 ‘ 𝑏 ) )
24 22 23 orbi12i ⊢ ( ( ( 𝑓 ‘ 𝑏 ) ◡ [⊊] ( 𝑓 ‘ suc 𝑏 ) ∨ ( 𝑓 ‘ 𝑏 ) = ( 𝑓 ‘ suc 𝑏 ) ) ↔ ( ( 𝑓 ‘ suc 𝑏 ) ⊊ ( 𝑓 ‘ 𝑏 ) ∨ ( 𝑓 ‘ suc 𝑏 ) = ( 𝑓 ‘ 𝑏 ) ) )
25 17 24 sylbb2 ⊢ ( ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) → ( ( 𝑓 ‘ 𝑏 ) ◡ [⊊] ( 𝑓 ‘ suc 𝑏 ) ∨ ( 𝑓 ‘ 𝑏 ) = ( 𝑓 ‘ suc 𝑏 ) ) )
26 25 ralimi ⊢ ( ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) → ∀ 𝑏 ∈ ω ( ( 𝑓 ‘ 𝑏 ) ◡ [⊊] ( 𝑓 ‘ suc 𝑏 ) ∨ ( 𝑓 ‘ 𝑏 ) = ( 𝑓 ‘ suc 𝑏 ) ) )
27 26 ad2antll ⊢ ( ( 𝐴 ∈ FinII ∧ ( 𝑓 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ) ) → ∀ 𝑏 ∈ ω ( ( 𝑓 ‘ 𝑏 ) ◡ [⊊] ( 𝑓 ‘ suc 𝑏 ) ∨ ( 𝑓 ‘ 𝑏 ) = ( 𝑓 ‘ suc 𝑏 ) ) )
28 porpss ⊢ [⊊] Po ran 𝑓
29 cnvpo ⊢ ( [⊊] Po ran 𝑓 ↔ ◡ [⊊] Po ran 𝑓 )
30 28 29 mpbi ⊢ ◡ [⊊] Po ran 𝑓
31 30 a1i ⊢ ( ( 𝐴 ∈ FinII ∧ ( 𝑓 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ) ) → ◡ [⊊] Po ran 𝑓 )
32 sornom ⊢ ( ( 𝑓 Fn ω ∧ ∀ 𝑏 ∈ ω ( ( 𝑓 ‘ 𝑏 ) ◡ [⊊] ( 𝑓 ‘ suc 𝑏 ) ∨ ( 𝑓 ‘ 𝑏 ) = ( 𝑓 ‘ suc 𝑏 ) ) ∧ ◡ [⊊] Po ran 𝑓 ) → ◡ [⊊] Or ran 𝑓 )
33 16 27 31 32 syl3anc ⊢ ( ( 𝐴 ∈ FinII ∧ ( 𝑓 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ) ) → ◡ [⊊] Or ran 𝑓 )
34 cnvso ⊢ ( [⊊] Or ran 𝑓 ↔ ◡ [⊊] Or ran 𝑓 )
35 33 34 sylibr ⊢ ( ( 𝐴 ∈ FinII ∧ ( 𝑓 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ) ) → [⊊] Or ran 𝑓 )
36 fin2i2 ⊢ ( ( ( 𝐴 ∈ FinII ∧ ran 𝑓 ⊆ 𝒫 𝐴 ) ∧ ( ran 𝑓 ≠ ∅ ∧ [⊊] Or ran 𝑓 ) ) → ∩ ran 𝑓 ∈ ran 𝑓 )
37 3 5 14 35 36 syl22anc ⊢ ( ( 𝐴 ∈ FinII ∧ ( 𝑓 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ) ) → ∩ ran 𝑓 ∈ ran 𝑓 )
38 37 expr ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑓 : ω ⟶ 𝒫 𝐴 ) → ( ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) )
39 2 38 sylan2 ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ) → ( ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) )
40 39 ralrimiva ⊢ ( 𝐴 ∈ FinII → ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) )
41 1 isfin3ds ⊢ ( 𝐴 ∈ FinII → ( 𝐴 ∈ 𝐹 ↔ ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) )
42 40 41 mpbird ⊢ ( 𝐴 ∈ FinII → 𝐴 ∈ 𝐹 )