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

Metamath Proof Explorer

Theorem fin67

Description: Every VI-finite set is VII-finite. (Contributed by Stefan O'Rear, 29-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin67 ( 𝐴 ∈ FinVI → 𝐴 ∈ FinVII )

Proof

Step Hyp Ref Expression
1 isfin6 ⊢ ( 𝐴 ∈ FinVI ↔ ( 𝐴 ≺ 2o ∨ 𝐴 ≺ ( 𝐴 × 𝐴 ) ) )
2 2onn ⊢ 2o ∈ ω
3 ssid ⊢ 2o ⊆ 2o
4 ssnnfi ⊢ ( ( 2o ∈ ω ∧ 2o ⊆ 2o ) → 2o ∈ Fin )
5 2 3 4 mp2an ⊢ 2o ∈ Fin
6 sdomdom ⊢ ( 𝐴 ≺ 2o → 𝐴 ≼ 2o )
7 domfi ⊢ ( ( 2o ∈ Fin ∧ 𝐴 ≼ 2o ) → 𝐴 ∈ Fin )
8 5 6 7 sylancr ⊢ ( 𝐴 ≺ 2o → 𝐴 ∈ Fin )
9 fin17 ⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ FinVII )
10 8 9 syl ⊢ ( 𝐴 ≺ 2o → 𝐴 ∈ FinVII )
11 sdomnen ⊢ ( 𝐴 ≺ ( 𝐴 × 𝐴 ) → ¬ 𝐴 ≈ ( 𝐴 × 𝐴 ) )
12 eldifi ⊢ ( 𝑏 ∈ ( On ∖ ω ) → 𝑏 ∈ On )
13 ensym ⊢ ( 𝐴 ≈ 𝑏 → 𝑏 ≈ 𝐴 )
14 isnumi ⊢ ( ( 𝑏 ∈ On ∧ 𝑏 ≈ 𝐴 ) → 𝐴 ∈ dom card )
15 12 13 14 syl2an ⊢ ( ( 𝑏 ∈ ( On ∖ ω ) ∧ 𝐴 ≈ 𝑏 ) → 𝐴 ∈ dom card )
16 vex ⊢ 𝑏 ∈ V
17 eldif ⊢ ( 𝑏 ∈ ( On ∖ ω ) ↔ ( 𝑏 ∈ On ∧ ¬ 𝑏 ∈ ω ) )
18 ordom ⊢ Ord ω
19 eloni ⊢ ( 𝑏 ∈ On → Ord 𝑏 )
20 ordtri1 ⊢ ( ( Ord ω ∧ Ord 𝑏 ) → ( ω ⊆ 𝑏 ↔ ¬ 𝑏 ∈ ω ) )
21 18 19 20 sylancr ⊢ ( 𝑏 ∈ On → ( ω ⊆ 𝑏 ↔ ¬ 𝑏 ∈ ω ) )
22 21 biimpar ⊢ ( ( 𝑏 ∈ On ∧ ¬ 𝑏 ∈ ω ) → ω ⊆ 𝑏 )
23 17 22 sylbi ⊢ ( 𝑏 ∈ ( On ∖ ω ) → ω ⊆ 𝑏 )
24 ssdomg ⊢ ( 𝑏 ∈ V → ( ω ⊆ 𝑏 → ω ≼ 𝑏 ) )
25 16 23 24 mpsyl ⊢ ( 𝑏 ∈ ( On ∖ ω ) → ω ≼ 𝑏 )
26 domen2 ⊢ ( 𝐴 ≈ 𝑏 → ( ω ≼ 𝐴 ↔ ω ≼ 𝑏 ) )
27 25 26 imbitrrid ⊢ ( 𝐴 ≈ 𝑏 → ( 𝑏 ∈ ( On ∖ ω ) → ω ≼ 𝐴 ) )
28 27 impcom ⊢ ( ( 𝑏 ∈ ( On ∖ ω ) ∧ 𝐴 ≈ 𝑏 ) → ω ≼ 𝐴 )
29 infxpidm2 ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )
30 15 28 29 syl2anc ⊢ ( ( 𝑏 ∈ ( On ∖ ω ) ∧ 𝐴 ≈ 𝑏 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )
31 ensym ⊢ ( ( 𝐴 × 𝐴 ) ≈ 𝐴 → 𝐴 ≈ ( 𝐴 × 𝐴 ) )
32 30 31 syl ⊢ ( ( 𝑏 ∈ ( On ∖ ω ) ∧ 𝐴 ≈ 𝑏 ) → 𝐴 ≈ ( 𝐴 × 𝐴 ) )
33 32 rexlimiva ⊢ ( ∃ 𝑏 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑏 → 𝐴 ≈ ( 𝐴 × 𝐴 ) )
34 11 33 nsyl ⊢ ( 𝐴 ≺ ( 𝐴 × 𝐴 ) → ¬ ∃ 𝑏 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑏 )
35 relsdom ⊢ Rel ≺
36 35 brrelex1i ⊢ ( 𝐴 ≺ ( 𝐴 × 𝐴 ) → 𝐴 ∈ V )
37 isfin7 ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ FinVII ↔ ¬ ∃ 𝑏 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑏 ) )
38 36 37 syl ⊢ ( 𝐴 ≺ ( 𝐴 × 𝐴 ) → ( 𝐴 ∈ FinVII ↔ ¬ ∃ 𝑏 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑏 ) )
39 34 38 mpbird ⊢ ( 𝐴 ≺ ( 𝐴 × 𝐴 ) → 𝐴 ∈ FinVII )
40 10 39 jaoi ⊢ ( ( 𝐴 ≺ 2o ∨ 𝐴 ≺ ( 𝐴 × 𝐴 ) ) → 𝐴 ∈ FinVII )
41 1 40 sylbi ⊢ ( 𝐴 ∈ FinVI → 𝐴 ∈ FinVII )