This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐴 ≈ 𝐵 )