hasheqf1oi

Description: The size of two sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 25-Dec-2017) (Revised by AV, 4-May-2021)

		Ref	Expression
	Assertion	hasheqf1oi	$⊢ A \in V \to (\exists f f : A \underset{1-1 onto}{⟶} B \to \|A\| = \|B\|)$

Proof

Step	Hyp	Ref	Expression
1		hasheqf1o	$⊢ (A \in Fin \land B \in Fin) \to (\|A\| = \|B\| \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} B)$
2	1	biimprd	$⊢ (A \in Fin \land B \in Fin) \to (\exists f f : A \underset{1-1 onto}{⟶} B \to \|A\| = \|B\|)$
3	2	a1d	$⊢ (A \in Fin \land B \in Fin) \to (A \in V \to (\exists f f : A \underset{1-1 onto}{⟶} B \to \|A\| = \|B\|))$
4		fiinfnf1o	$⊢ (A \in Fin \land \neg B \in Fin) \to \neg \exists f f : A \underset{1-1 onto}{⟶} B$
5	4	pm2.21d	$⊢ (A \in Fin \land \neg B \in Fin) \to (\exists f f : A \underset{1-1 onto}{⟶} B \to \|A\| = \|B\|)$
6	5	a1d	$⊢ (A \in Fin \land \neg B \in Fin) \to (A \in V \to (\exists f f : A \underset{1-1 onto}{⟶} B \to \|A\| = \|B\|))$
7		fiinfnf1o	$⊢ (B \in Fin \land \neg A \in Fin) \to \neg \exists g g : B \underset{1-1 onto}{⟶} A$
8		19.41v	$⊢ \exists f (f : A \underset{1-1 onto}{⟶} B \land A \in V) \leftrightarrow (\exists f f : A \underset{1-1 onto}{⟶} B \land A \in V)$
9		f1orel	$⊢ f : A \underset{1-1 onto}{⟶} B \to Rel f$
10	9	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} B \land A \in V) \to Rel f$
11		f1ocnvb	$⊢ Rel f \to (f : A \underset{1-1 onto}{⟶} B \leftrightarrow f^{-1} : B \underset{1-1 onto}{⟶} A)$
12	10 11	syl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land A \in V) \to (f : A \underset{1-1 onto}{⟶} B \leftrightarrow f^{-1} : B \underset{1-1 onto}{⟶} A)$
13		f1of	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A ⟶ B$
14		fex	$⊢ (f : A ⟶ B \land A \in V) \to f \in V$
15	13 14	sylan	$⊢ (f : A \underset{1-1 onto}{⟶} B \land A \in V) \to f \in V$
16		cnvexg	$⊢ f \in V \to f^{-1} \in V$
17		f1oeq1	$⊢ g = f^{-1} \to (g : B \underset{1-1 onto}{⟶} A \leftrightarrow f^{-1} : B \underset{1-1 onto}{⟶} A)$
18	17	spcegv	$⊢ f^{-1} \in V \to (f^{-1} : B \underset{1-1 onto}{⟶} A \to \exists g g : B \underset{1-1 onto}{⟶} A)$
19	15 16 18	3syl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land A \in V) \to (f^{-1} : B \underset{1-1 onto}{⟶} A \to \exists g g : B \underset{1-1 onto}{⟶} A)$
20		pm2.24	$⊢ \exists g g : B \underset{1-1 onto}{⟶} A \to (\neg \exists g g : B \underset{1-1 onto}{⟶} A \to \|A\| = \|B\|)$
21	19 20	syl6	$⊢ (f : A \underset{1-1 onto}{⟶} B \land A \in V) \to (f^{-1} : B \underset{1-1 onto}{⟶} A \to (\neg \exists g g : B \underset{1-1 onto}{⟶} A \to \|A\| = \|B\|))$
22	12 21	sylbid	$⊢ (f : A \underset{1-1 onto}{⟶} B \land A \in V) \to (f : A \underset{1-1 onto}{⟶} B \to (\neg \exists g g : B \underset{1-1 onto}{⟶} A \to \|A\| = \|B\|))$
23	22	com12	$⊢ f : A \underset{1-1 onto}{⟶} B \to ((f : A \underset{1-1 onto}{⟶} B \land A \in V) \to (\neg \exists g g : B \underset{1-1 onto}{⟶} A \to \|A\| = \|B\|))$
24	23	anabsi5	$⊢ (f : A \underset{1-1 onto}{⟶} B \land A \in V) \to (\neg \exists g g : B \underset{1-1 onto}{⟶} A \to \|A\| = \|B\|)$
25	24	exlimiv	$⊢ \exists f (f : A \underset{1-1 onto}{⟶} B \land A \in V) \to (\neg \exists g g : B \underset{1-1 onto}{⟶} A \to \|A\| = \|B\|)$
26	8 25	sylbir	$⊢ (\exists f f : A \underset{1-1 onto}{⟶} B \land A \in V) \to (\neg \exists g g : B \underset{1-1 onto}{⟶} A \to \|A\| = \|B\|)$
27	26	ex	$⊢ \exists f f : A \underset{1-1 onto}{⟶} B \to (A \in V \to (\neg \exists g g : B \underset{1-1 onto}{⟶} A \to \|A\| = \|B\|))$
28	27	com13	$⊢ \neg \exists g g : B \underset{1-1 onto}{⟶} A \to (A \in V \to (\exists f f : A \underset{1-1 onto}{⟶} B \to \|A\| = \|B\|))$
29	7 28	syl	$⊢ (B \in Fin \land \neg A \in Fin) \to (A \in V \to (\exists f f : A \underset{1-1 onto}{⟶} B \to \|A\| = \|B\|))$
30	29	ancoms	$⊢ (\neg A \in Fin \land B \in Fin) \to (A \in V \to (\exists f f : A \underset{1-1 onto}{⟶} B \to \|A\| = \|B\|))$
31		hashinf	$⊢ (A \in V \land \neg A \in Fin) \to \|A\| = +∞$
32	31	expcom	$⊢ \neg A \in Fin \to (A \in V \to \|A\| = +∞)$
33	32	adantr	$⊢ (\neg A \in Fin \land \neg B \in Fin) \to (A \in V \to \|A\| = +∞)$
34	33	imp	$⊢ ((\neg A \in Fin \land \neg B \in Fin) \land A \in V) \to \|A\| = +∞$
35	34	adantr	$⊢ (((\neg A \in Fin \land \neg B \in Fin) \land A \in V) \land f : A \underset{1-1 onto}{⟶} B) \to \|A\| = +∞$
36		simpr	$⊢ ((\neg A \in Fin \land \neg B \in Fin) \land A \in V) \to A \in V$
37		f1ofo	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{onto}{⟶} B$
38		focdmex	$⊢ A \in V \to (f : A \underset{onto}{⟶} B \to B \in V)$
39	38	imp	$⊢ (A \in V \land f : A \underset{onto}{⟶} B) \to B \in V$
40	36 37 39	syl2an	$⊢ (((\neg A \in Fin \land \neg B \in Fin) \land A \in V) \land f : A \underset{1-1 onto}{⟶} B) \to B \in V$
41		hashinf	$⊢ (B \in V \land \neg B \in Fin) \to \|B\| = +∞$
42	41	expcom	$⊢ \neg B \in Fin \to (B \in V \to \|B\| = +∞)$
43	42	ad3antlr	$⊢ (((\neg A \in Fin \land \neg B \in Fin) \land A \in V) \land f : A \underset{1-1 onto}{⟶} B) \to (B \in V \to \|B\| = +∞)$
44	40 43	mpd	$⊢ (((\neg A \in Fin \land \neg B \in Fin) \land A \in V) \land f : A \underset{1-1 onto}{⟶} B) \to \|B\| = +∞$
45	35 44	eqtr4d	$⊢ (((\neg A \in Fin \land \neg B \in Fin) \land A \in V) \land f : A \underset{1-1 onto}{⟶} B) \to \|A\| = \|B\|$
46	45	ex	$⊢ ((\neg A \in Fin \land \neg B \in Fin) \land A \in V) \to (f : A \underset{1-1 onto}{⟶} B \to \|A\| = \|B\|)$
47	46	exlimdv	$⊢ ((\neg A \in Fin \land \neg B \in Fin) \land A \in V) \to (\exists f f : A \underset{1-1 onto}{⟶} B \to \|A\| = \|B\|)$
48	47	ex	$⊢ (\neg A \in Fin \land \neg B \in Fin) \to (A \in V \to (\exists f f : A \underset{1-1 onto}{⟶} B \to \|A\| = \|B\|))$
49	3 6 30 48	4cases	$⊢ A \in V \to (\exists f f : A \underset{1-1 onto}{⟶} B \to \|A\| = \|B\|)$

Metamath Proof Explorer

Theorem hasheqf1oi

Proof