Theorem hasheqf1od

Description: The size of two sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by AV, 4-May-2021)

	Ref	Expression
Hypotheses	hasheqf1od.a	$$⊢\phi \to A\in U$$
	hasheqf1od.f	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$
Assertion	hasheqf1od	$$⊢\phi \to \left|A\right|=\left|B\right|$$

Proof

Step	Hyp	Ref	Expression
1		hasheqf1od.a	$$⊢\phi \to A\in U$$
2		hasheqf1od.f	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$
3		f1of	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F:A⟶B$$
4	2 3	syl	$$⊢\phi \to F:A⟶B$$
5	4 1	fexd	$$⊢\phi \to F\in \mathrm{V}$$
6		f1oeq1	$$⊢f=F\to \left(f:A\underset{1-1\; onto}{⟶}B\leftrightarrow F:A\underset{1-1\; onto}{⟶}B\right)$$
7	5 2 6	spcedv	$$⊢\phi \to \exists ff:A\underset{1-1\; onto}{⟶}B$$
8		hasheqf1oi	$$⊢A\in U\to \left(\exists ff:A\underset{1-1\; onto}{⟶}B\to \left|A\right|=\left|B\right|\right)$$
9	1 7 8	sylc	$$⊢\phi \to \left|A\right|=\left|B\right|$$