Theorem en3d

Description: Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004) (Revised by Mario Carneiro, 12-May-2014) (Revised by AV, 4-Aug-2024)

	Ref	Expression
Hypotheses	en3d.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	en3d.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	en3d.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )
	en3d.4	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴 ) )
	en3d.5	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = 𝐷 ↔ 𝑦 = 𝐶 ) ) )
Assertion	en3d	⊢ ( 𝜑 → 𝐴 ≈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		en3d.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		en3d.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		en3d.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )
4		en3d.4	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴 ) )
5		en3d.5	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = 𝐷 ↔ 𝑦 = 𝐶 ) ) )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
7	3	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
8	4	imp	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝐴 )
9	5	imp	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 = 𝐷 ↔ 𝑦 = 𝐶 ) )
10	6 7 8 9	f1o2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1-onto→ 𝐵 )
11		f1oen2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 )
12	1 2 10 11	syl3anc	⊢ ( 𝜑 → 𝐴 ≈ 𝐵 )