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		fex	$$⊢\left(F:A⟶B\wedge A\in U\right)\to F\in \mathrm{V}$$
6	4 1 5	syl2anc	$$⊢\phi \to F\in \mathrm{V}$$
7		f1oeq1	$$⊢f=F\to \left(f:A\underset{1-1\; onto}{⟶}B\leftrightarrow F:A\underset{1-1\; onto}{⟶}B\right)$$
8	6 2 7	spcedv	$$⊢\phi \to \exists ff:A\underset{1-1\; onto}{⟶}B$$
9		hasheqf1oi	$$⊢A\in U\to \left(\exists ff:A\underset{1-1\; onto}{⟶}B\to \left|A\right|=\left|B\right|\right)$$
10	1 8 9	sylc	$$⊢\phi \to \left|A\right|=\left|B\right|$$