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	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	hasheqf1od.f	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
Assertion	hasheqf1od	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		hasheqf1od.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
2		hasheqf1od.f	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
3		f1of	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
4	2 3	syl	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
5		fex	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑈 ) → 𝐹 ∈ V )
6	4 1 5	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ V )
7		f1oeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) )
8	6 2 7	spcedv	⊢ ( 𝜑 → ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
9		hasheqf1oi	⊢ ( 𝐴 ∈ 𝑈 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )
10	1 8 9	sylc	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )