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 )