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 )