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

Metamath Proof Explorer

Theorem fin56

Description: Every V-finite set is VI-finite because multiplication dominates addition for cardinals. (Contributed by Stefan O'Rear, 29-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin56 ( 𝐴 ∈ FinV → 𝐴 ∈ FinVI )

Proof

Step Hyp Ref Expression
1 orc ⊢ ( 𝐴 = ∅ → ( 𝐴 = ∅ ∨ 𝐴 ≈ 1o ) )
2 sdom2en01 ⊢ ( 𝐴 ≺ 2o ↔ ( 𝐴 = ∅ ∨ 𝐴 ≈ 1o ) )
3 1 2 sylibr ⊢ ( 𝐴 = ∅ → 𝐴 ≺ 2o )
4 3 orcd ⊢ ( 𝐴 = ∅ → ( 𝐴 ≺ 2o ∨ 𝐴 ≺ ( 𝐴 × 𝐴 ) ) )
5 onfin2 ⊢ ω = ( On ∩ Fin )
6 inss2 ⊢ ( On ∩ Fin ) ⊆ Fin
7 5 6 eqsstri ⊢ ω ⊆ Fin
8 2onn ⊢ 2o ∈ ω
9 7 8 sselii ⊢ 2o ∈ Fin
10 relsdom ⊢ Rel ≺
11 10 brrelex1i ⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) → 𝐴 ∈ V )
12 fidomtri ⊢ ( ( 2o ∈ Fin ∧ 𝐴 ∈ V ) → ( 2o ≼ 𝐴 ↔ ¬ 𝐴 ≺ 2o ) )
13 9 11 12 sylancr ⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) → ( 2o ≼ 𝐴 ↔ ¬ 𝐴 ≺ 2o ) )
14 xp2dju ⊢ ( 2o × 𝐴 ) = ( 𝐴 ⊔ 𝐴 )
15 xpdom1g ⊢ ( ( 𝐴 ∈ V ∧ 2o ≼ 𝐴 ) → ( 2o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) )
16 11 15 sylan ⊢ ( ( 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ∧ 2o ≼ 𝐴 ) → ( 2o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) )
17 14 16 eqbrtrrid ⊢ ( ( 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ∧ 2o ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 × 𝐴 ) )
18 sdomdomtr ⊢ ( ( 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ∧ ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 × 𝐴 ) ) → 𝐴 ≺ ( 𝐴 × 𝐴 ) )
19 17 18 syldan ⊢ ( ( 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ∧ 2o ≼ 𝐴 ) → 𝐴 ≺ ( 𝐴 × 𝐴 ) )
20 19 ex ⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) → ( 2o ≼ 𝐴 → 𝐴 ≺ ( 𝐴 × 𝐴 ) ) )
21 13 20 sylbird ⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) → ( ¬ 𝐴 ≺ 2o → 𝐴 ≺ ( 𝐴 × 𝐴 ) ) )
22 21 orrd ⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) → ( 𝐴 ≺ 2o ∨ 𝐴 ≺ ( 𝐴 × 𝐴 ) ) )
23 4 22 jaoi ⊢ ( ( 𝐴 = ∅ ∨ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) → ( 𝐴 ≺ 2o ∨ 𝐴 ≺ ( 𝐴 × 𝐴 ) ) )
24 isfin5 ⊢ ( 𝐴 ∈ FinV ↔ ( 𝐴 = ∅ ∨ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) )
25 isfin6 ⊢ ( 𝐴 ∈ FinVI ↔ ( 𝐴 ≺ 2o ∨ 𝐴 ≺ ( 𝐴 × 𝐴 ) ) )
26 23 24 25 3imtr4i ⊢ ( 𝐴 ∈ FinV → 𝐴 ∈ FinVI )