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	4 1	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
6		f1oeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) )
7	5 2 6	spcedv	⊢ ( 𝜑 → ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
8		hasheqf1oi	⊢ ( 𝐴 ∈ 𝑈 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )
9	1 7 8	sylc	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )