Metamath Proof Explorer

Theorem dfres3

Description: Alternate definition of restriction. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion dfres3 ( 𝐴 ↾ 𝐵 ) = ( 𝐴 ∩ ( 𝐵 × ran 𝐴 ) )

Proof

Step Hyp Ref Expression
1 df-res ⊢ ( 𝐴 ↾ 𝐵 ) = ( 𝐴 ∩ ( 𝐵 × V ) )
2 eleq1 ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑥 ∈ 𝐴 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ) )
3 vex ⊢ 𝑧 ∈ V
4 3 biantru ⊢ ( 𝑦 ∈ 𝐵 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V ) )
5 vex ⊢ 𝑦 ∈ V
6 5 3 opelrn ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 → 𝑧 ∈ ran 𝐴 )
7 6 biantrud ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 → ( 𝑦 ∈ 𝐵 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴 ) ) )
8 4 7 bitr3id ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴 ) ) )
9 2 8 syl6bi ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑥 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴 ) ) ) )
10 9 com12 ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴 ) ) ) )
11 10 pm5.32d ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V ) ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴 ) ) ) )
12 11 2exbidv ⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V ) ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴 ) ) ) )
13 elxp ⊢ ( 𝑥 ∈ ( 𝐵 × V ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V ) ) )
14 elxp ⊢ ( 𝑥 ∈ ( 𝐵 × ran 𝐴 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴 ) ) )
15 12 13 14 3bitr4g ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( 𝐵 × V ) ↔ 𝑥 ∈ ( 𝐵 × ran 𝐴 ) ) )
16 15 pm5.32i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × V ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × ran 𝐴 ) ) )
17 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 × ran 𝐴 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × ran 𝐴 ) ) )
18 16 17 bitr4i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × V ) ) ↔ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 × ran 𝐴 ) ) )
19 18 ineqri ⊢ ( 𝐴 ∩ ( 𝐵 × V ) ) = ( 𝐴 ∩ ( 𝐵 × ran 𝐴 ) )
20 1 19 eqtri ⊢ ( 𝐴 ↾ 𝐵 ) = ( 𝐴 ∩ ( 𝐵 × ran 𝐴 ) )