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

Metamath Proof Explorer

Theorem dminxp

Description: Two ways to express totality of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by NM, 17-Jan-2006)

Ref Expression
Assertion dminxp ( dom ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 𝐶 𝑦 )

Proof

Step Hyp Ref Expression
1 dfdm4 ⊢ dom ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = ran ◡ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) )
2 cnvin ⊢ ◡ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = ( ◡ 𝐶 ∩ ◡ ( 𝐴 × 𝐵 ) )
3 cnvxp ⊢ ◡ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 )
4 3 ineq2i ⊢ ( ◡ 𝐶 ∩ ◡ ( 𝐴 × 𝐵 ) ) = ( ◡ 𝐶 ∩ ( 𝐵 × 𝐴 ) )
5 2 4 eqtri ⊢ ◡ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = ( ◡ 𝐶 ∩ ( 𝐵 × 𝐴 ) )
6 5 rneqi ⊢ ran ◡ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = ran ( ◡ 𝐶 ∩ ( 𝐵 × 𝐴 ) )
7 1 6 eqtri ⊢ dom ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = ran ( ◡ 𝐶 ∩ ( 𝐵 × 𝐴 ) )
8 7 eqeq1i ⊢ ( dom ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = 𝐴 ↔ ran ( ◡ 𝐶 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 )
9 rninxp ⊢ ( ran ( ◡ 𝐶 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 ◡ 𝐶 𝑥 )
10 vex ⊢ 𝑦 ∈ V
11 vex ⊢ 𝑥 ∈ V
12 10 11 brcnv ⊢ ( 𝑦 ◡ 𝐶 𝑥 ↔ 𝑥 𝐶 𝑦 )
13 12 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐵 𝑦 ◡ 𝐶 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑥 𝐶 𝑦 )
14 13 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 ◡ 𝐶 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 𝐶 𝑦 )
15 8 9 14 3bitri ⊢ ( dom ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 𝐶 𝑦 )