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	$⊢ A \in {Fin}^{IV} \to A \in {Fin}^{V}$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \neq \emptyset \land A \approx (A ⊔︀ A)) \to A \neq \emptyset$
2		relen	$⊢ Rel \approx$
3	2	brrelex1i	$⊢ A \approx (A ⊔︀ A) \to A \in V$
4	3	adantl	$⊢ (A \neq \emptyset \land A \approx (A ⊔︀ A)) \to A \in V$
5		0sdomg	$⊢ A \in V \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
6	4 5	syl	$⊢ (A \neq \emptyset \land A \approx (A ⊔︀ A)) \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
7	1 6	mpbird	$⊢ (A \neq \emptyset \land A \approx (A ⊔︀ A)) \to \emptyset ≺ A$
8		0sdom1dom	$⊢ \emptyset ≺ A \leftrightarrow 1_{𝑜} ≼ A$
9	7 8	sylib	$⊢ (A \neq \emptyset \land A \approx (A ⊔︀ A)) \to 1_{𝑜} ≼ A$
10		djudom2	$⊢ (1_{𝑜} ≼ A \land A \in V) \to (A ⊔︀ 1_{𝑜}) ≼ (A ⊔︀ A)$
11	9 4 10	syl2anc	$⊢ (A \neq \emptyset \land A \approx (A ⊔︀ A)) \to (A ⊔︀ 1_{𝑜}) ≼ (A ⊔︀ A)$
12		domen2	$⊢ A \approx (A ⊔︀ A) \to ((A ⊔︀ 1_{𝑜}) ≼ A \leftrightarrow (A ⊔︀ 1_{𝑜}) ≼ (A ⊔︀ A))$
13	12	adantl	$⊢ (A \neq \emptyset \land A \approx (A ⊔︀ A)) \to ((A ⊔︀ 1_{𝑜}) ≼ A \leftrightarrow (A ⊔︀ 1_{𝑜}) ≼ (A ⊔︀ A))$
14	11 13	mpbird	$⊢ (A \neq \emptyset \land A \approx (A ⊔︀ A)) \to (A ⊔︀ 1_{𝑜}) ≼ A$
15		domnsym	$⊢ (A ⊔︀ 1_{𝑜}) ≼ A \to \neg A ≺ (A ⊔︀ 1_{𝑜})$
16	14 15	syl	$⊢ (A \neq \emptyset \land A \approx (A ⊔︀ A)) \to \neg A ≺ (A ⊔︀ 1_{𝑜})$
17		isfin4p1	$⊢ A \in {Fin}^{IV} \leftrightarrow A ≺ (A ⊔︀ 1_{𝑜})$
18	17	biimpi	$⊢ A \in {Fin}^{IV} \to A ≺ (A ⊔︀ 1_{𝑜})$
19	16 18	nsyl3	$⊢ A \in {Fin}^{IV} \to \neg (A \neq \emptyset \land A \approx (A ⊔︀ A))$
20		isfin5-2	$⊢ A \in {Fin}^{IV} \to (A \in {Fin}^{V} \leftrightarrow \neg (A \neq \emptyset \land A \approx (A ⊔︀ A)))$
21	19 20	mpbird	$⊢ A \in {Fin}^{IV} \to A \in {Fin}^{V}$

Metamath Proof Explorer

Theorem fin45

Proof