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 | en2d.1 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | |
| en2d.2 | ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 ) | ||
| en2d.3 | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝑋 ) ) | ||
| en2d.4 | ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → 𝐷 ∈ 𝑌 ) ) | ||
| en2d.5 | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) ) | ||
| Assertion | en2d | ⊢ ( 𝜑 → 𝐴 ≈ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | en2d.1 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | |
| 2 | en2d.2 | ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 ) | |
| 3 | en2d.3 | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝑋 ) ) | |
| 4 | en2d.4 | ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → 𝐷 ∈ 𝑌 ) ) | |
| 5 | en2d.5 | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷 ) ) ) | |
| 6 | eqid | ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) | |
| 7 | 3 | imp | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑋 ) |
| 8 | 4 | imp | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝑌 ) |
| 9 | 6 7 8 5 | f1od | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1-onto→ 𝐵 ) |
| 10 | f1oen2g | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 ) | |
| 11 | 1 2 9 10 | syl3anc | ⊢ ( 𝜑 → 𝐴 ≈ 𝐵 ) |