Description: Two ways to express surjectivity of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by NM, 17-Jan-2006) (Proof shortened by Andrew Salmon, 27-Aug-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rninxp | ⊢ ( ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝐶 𝑦 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfss3 | ⊢ ( 𝐵 ⊆ ran ( 𝐶 ↾ 𝐴 ) ↔ ∀ 𝑦 ∈ 𝐵 𝑦 ∈ ran ( 𝐶 ↾ 𝐴 ) ) | |
| 2 | ssrnres | ⊢ ( 𝐵 ⊆ ran ( 𝐶 ↾ 𝐴 ) ↔ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ) | |
| 3 | df-ima | ⊢ ( 𝐶 “ 𝐴 ) = ran ( 𝐶 ↾ 𝐴 ) | |
| 4 | 3 | eleq2i | ⊢ ( 𝑦 ∈ ( 𝐶 “ 𝐴 ) ↔ 𝑦 ∈ ran ( 𝐶 ↾ 𝐴 ) ) |
| 5 | vex | ⊢ 𝑦 ∈ V | |
| 6 | 5 | elima | ⊢ ( 𝑦 ∈ ( 𝐶 “ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝐶 𝑦 ) |
| 7 | 4 6 | bitr3i | ⊢ ( 𝑦 ∈ ran ( 𝐶 ↾ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝐶 𝑦 ) |
| 8 | 7 | ralbii | ⊢ ( ∀ 𝑦 ∈ 𝐵 𝑦 ∈ ran ( 𝐶 ↾ 𝐴 ) ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝐶 𝑦 ) |
| 9 | 1 2 8 | 3bitr3i | ⊢ ( ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝐶 𝑦 ) |