Metamath Proof Explorer


Theorem fin45

Description: Every IV-finite set is V-finite: if we can pack two copies of the set into itself, we can certainly leave space. (Contributed by Stefan O'Rear, 30-Oct-2014) (Proof shortened by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion fin45 ( 𝐴 ∈ FinIV𝐴 ∈ FinV )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≈ ( 𝐴𝐴 ) ) → 𝐴 ≠ ∅ )
2 relen Rel ≈
3 2 brrelex1i ( 𝐴 ≈ ( 𝐴𝐴 ) → 𝐴 ∈ V )
4 3 adantl ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≈ ( 𝐴𝐴 ) ) → 𝐴 ∈ V )
5 0sdomg ( 𝐴 ∈ V → ( ∅ ≺ 𝐴𝐴 ≠ ∅ ) )
6 4 5 syl ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≈ ( 𝐴𝐴 ) ) → ( ∅ ≺ 𝐴𝐴 ≠ ∅ ) )
7 1 6 mpbird ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≈ ( 𝐴𝐴 ) ) → ∅ ≺ 𝐴 )
8 0sdom1dom ( ∅ ≺ 𝐴 ↔ 1o𝐴 )
9 7 8 sylib ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≈ ( 𝐴𝐴 ) ) → 1o𝐴 )
10 djudom2 ( ( 1o𝐴𝐴 ∈ V ) → ( 𝐴 ⊔ 1o ) ≼ ( 𝐴𝐴 ) )
11 9 4 10 syl2anc ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≈ ( 𝐴𝐴 ) ) → ( 𝐴 ⊔ 1o ) ≼ ( 𝐴𝐴 ) )
12 domen2 ( 𝐴 ≈ ( 𝐴𝐴 ) → ( ( 𝐴 ⊔ 1o ) ≼ 𝐴 ↔ ( 𝐴 ⊔ 1o ) ≼ ( 𝐴𝐴 ) ) )
13 12 adantl ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≈ ( 𝐴𝐴 ) ) → ( ( 𝐴 ⊔ 1o ) ≼ 𝐴 ↔ ( 𝐴 ⊔ 1o ) ≼ ( 𝐴𝐴 ) ) )
14 11 13 mpbird ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≈ ( 𝐴𝐴 ) ) → ( 𝐴 ⊔ 1o ) ≼ 𝐴 )
15 domnsym ( ( 𝐴 ⊔ 1o ) ≼ 𝐴 → ¬ 𝐴 ≺ ( 𝐴 ⊔ 1o ) )
16 14 15 syl ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≈ ( 𝐴𝐴 ) ) → ¬ 𝐴 ≺ ( 𝐴 ⊔ 1o ) )
17 isfin4p1 ( 𝐴 ∈ FinIV𝐴 ≺ ( 𝐴 ⊔ 1o ) )
18 17 biimpi ( 𝐴 ∈ FinIV𝐴 ≺ ( 𝐴 ⊔ 1o ) )
19 16 18 nsyl3 ( 𝐴 ∈ FinIV → ¬ ( 𝐴 ≠ ∅ ∧ 𝐴 ≈ ( 𝐴𝐴 ) ) )
20 isfin5-2 ( 𝐴 ∈ FinIV → ( 𝐴 ∈ FinV ↔ ¬ ( 𝐴 ≠ ∅ ∧ 𝐴 ≈ ( 𝐴𝐴 ) ) ) )
21 19 20 mpbird ( 𝐴 ∈ FinIV𝐴 ∈ FinV )