fin4en1

Description: Dedekind finite is a cardinal property. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 16-May-2015)

		Ref	Expression
	Assertion	fin4en1	$⊢ A \approx B \to (A \in {Fin}^{IV} \to B \in {Fin}^{IV})$

Proof

Step	Hyp	Ref	Expression
1		ensym	$⊢ A \approx B \to B \approx A$
2		bren	$⊢ B \approx A \leftrightarrow \exists f f : B \underset{1-1 onto}{⟶} A$
3		simpr	$⊢ (f : B \underset{1-1 onto}{⟶} A \land x \subset B) \to x \subset B$
4		f1of1	$⊢ f : B \underset{1-1 onto}{⟶} A \to f : B \underset{1-1}{⟶} A$
5		pssss	$⊢ x \subset B \to x \subseteq B$
6		ssid	$⊢ B \subseteq B$
7	5 6	jctir	$⊢ x \subset B \to (x \subseteq B \land B \subseteq B)$
8		f1imapss	$⊢ (f : B \underset{1-1}{⟶} A \land (x \subseteq B \land B \subseteq B)) \to (f [x] \subset f [B] \leftrightarrow x \subset B)$
9	4 7 8	syl2an	$⊢ (f : B \underset{1-1 onto}{⟶} A \land x \subset B) \to (f [x] \subset f [B] \leftrightarrow x \subset B)$
10	3 9	mpbird	$⊢ (f : B \underset{1-1 onto}{⟶} A \land x \subset B) \to f [x] \subset f [B]$
11		imadmrn	$⊢ f [dom f] = ran f$
12		f1odm	$⊢ f : B \underset{1-1 onto}{⟶} A \to dom f = B$
13	12	imaeq2d	$⊢ f : B \underset{1-1 onto}{⟶} A \to f [dom f] = f [B]$
14		dff1o5	$⊢ f : B \underset{1-1 onto}{⟶} A \leftrightarrow (f : B \underset{1-1}{⟶} A \land ran f = A)$
15	14	simprbi	$⊢ f : B \underset{1-1 onto}{⟶} A \to ran f = A$
16	11 13 15	3eqtr3a	$⊢ f : B \underset{1-1 onto}{⟶} A \to f [B] = A$
17	16	adantr	$⊢ (f : B \underset{1-1 onto}{⟶} A \land x \subset B) \to f [B] = A$
18	17	psseq2d	$⊢ (f : B \underset{1-1 onto}{⟶} A \land x \subset B) \to (f [x] \subset f [B] \leftrightarrow f [x] \subset A)$
19	10 18	mpbid	$⊢ (f : B \underset{1-1 onto}{⟶} A \land x \subset B) \to f [x] \subset A$
20	19	adantrr	$⊢ (f : B \underset{1-1 onto}{⟶} A \land (x \subset B \land x \approx B)) \to f [x] \subset A$
21		vex	$⊢ x \in V$
22	21	f1imaen	$⊢ (f : B \underset{1-1}{⟶} A \land x \subseteq B) \to f [x] \approx x$
23	4 5 22	syl2an	$⊢ (f : B \underset{1-1 onto}{⟶} A \land x \subset B) \to f [x] \approx x$
24	23	adantrr	$⊢ (f : B \underset{1-1 onto}{⟶} A \land (x \subset B \land x \approx B)) \to f [x] \approx x$
25		simprr	$⊢ (f : B \underset{1-1 onto}{⟶} A \land (x \subset B \land x \approx B)) \to x \approx B$
26		entr	$⊢ (f [x] \approx x \land x \approx B) \to f [x] \approx B$
27	24 25 26	syl2anc	$⊢ (f : B \underset{1-1 onto}{⟶} A \land (x \subset B \land x \approx B)) \to f [x] \approx B$
28		vex	$⊢ f \in V$
29		f1oen3g	$⊢ (f \in V \land f : B \underset{1-1 onto}{⟶} A) \to B \approx A$
30	28 29	mpan	$⊢ f : B \underset{1-1 onto}{⟶} A \to B \approx A$
31	30	adantr	$⊢ (f : B \underset{1-1 onto}{⟶} A \land (x \subset B \land x \approx B)) \to B \approx A$
32		entr	$⊢ (f [x] \approx B \land B \approx A) \to f [x] \approx A$
33	27 31 32	syl2anc	$⊢ (f : B \underset{1-1 onto}{⟶} A \land (x \subset B \land x \approx B)) \to f [x] \approx A$
34		fin4i	$⊢ (f [x] \subset A \land f [x] \approx A) \to \neg A \in {Fin}^{IV}$
35	20 33 34	syl2anc	$⊢ (f : B \underset{1-1 onto}{⟶} A \land (x \subset B \land x \approx B)) \to \neg A \in {Fin}^{IV}$
36	35	ex	$⊢ f : B \underset{1-1 onto}{⟶} A \to ((x \subset B \land x \approx B) \to \neg A \in {Fin}^{IV})$
37	36	exlimdv	$⊢ f : B \underset{1-1 onto}{⟶} A \to (\exists x (x \subset B \land x \approx B) \to \neg A \in {Fin}^{IV})$
38	37	con2d	$⊢ f : B \underset{1-1 onto}{⟶} A \to (A \in {Fin}^{IV} \to \neg \exists x (x \subset B \land x \approx B))$
39	38	exlimiv	$⊢ \exists f f : B \underset{1-1 onto}{⟶} A \to (A \in {Fin}^{IV} \to \neg \exists x (x \subset B \land x \approx B))$
40	2 39	sylbi	$⊢ B \approx A \to (A \in {Fin}^{IV} \to \neg \exists x (x \subset B \land x \approx B))$
41		relen	$⊢ Rel \approx$
42	41	brrelex1i	$⊢ B \approx A \to B \in V$
43		isfin4	$⊢ B \in V \to (B \in {Fin}^{IV} \leftrightarrow \neg \exists x (x \subset B \land x \approx B))$
44	42 43	syl	$⊢ B \approx A \to (B \in {Fin}^{IV} \leftrightarrow \neg \exists x (x \subset B \land x \approx B))$
45	40 44	sylibrd	$⊢ B \approx A \to (A \in {Fin}^{IV} \to B \in {Fin}^{IV})$
46	1 45	syl	$⊢ A \approx B \to (A \in {Fin}^{IV} \to B \in {Fin}^{IV})$

Metamath Proof Explorer

Theorem fin4en1

Proof