Metamath Proof Explorer

Theorem oprssov

Description: The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007)

Ref Expression
Assertion oprssov ( ( ( Fun 𝐹 ∧ 𝐺 Fn ( 𝐶 × 𝐷 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → ( 𝐴 𝐹 𝐵 ) = ( 𝐴 𝐺 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ovres ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ( 𝐹 ↾ ( 𝐶 × 𝐷 ) ) 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )
2 1 adantl ⊢ ( ( ( Fun 𝐹 ∧ 𝐺 Fn ( 𝐶 × 𝐷 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → ( 𝐴 ( 𝐹 ↾ ( 𝐶 × 𝐷 ) ) 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )
3 fndm ⊢ ( 𝐺 Fn ( 𝐶 × 𝐷 ) → dom 𝐺 = ( 𝐶 × 𝐷 ) )
4 3 reseq2d ⊢ ( 𝐺 Fn ( 𝐶 × 𝐷 ) → ( 𝐹 ↾ dom 𝐺 ) = ( 𝐹 ↾ ( 𝐶 × 𝐷 ) ) )
5 4 3ad2ant2 ⊢ ( ( Fun 𝐹 ∧ 𝐺 Fn ( 𝐶 × 𝐷 ) ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐹 ↾ dom 𝐺 ) = ( 𝐹 ↾ ( 𝐶 × 𝐷 ) ) )
6 funssres ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐹 ↾ dom 𝐺 ) = 𝐺 )
7 6 3adant2 ⊢ ( ( Fun 𝐹 ∧ 𝐺 Fn ( 𝐶 × 𝐷 ) ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐹 ↾ dom 𝐺 ) = 𝐺 )
8 5 7 eqtr3d ⊢ ( ( Fun 𝐹 ∧ 𝐺 Fn ( 𝐶 × 𝐷 ) ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐹 ↾ ( 𝐶 × 𝐷 ) ) = 𝐺 )
9 8 oveqd ⊢ ( ( Fun 𝐹 ∧ 𝐺 Fn ( 𝐶 × 𝐷 ) ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐴 ( 𝐹 ↾ ( 𝐶 × 𝐷 ) ) 𝐵 ) = ( 𝐴 𝐺 𝐵 ) )
10 9 adantr ⊢ ( ( ( Fun 𝐹 ∧ 𝐺 Fn ( 𝐶 × 𝐷 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → ( 𝐴 ( 𝐹 ↾ ( 𝐶 × 𝐷 ) ) 𝐵 ) = ( 𝐴 𝐺 𝐵 ) )
11 2 10 eqtr3d ⊢ ( ( ( Fun 𝐹 ∧ 𝐺 Fn ( 𝐶 × 𝐷 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → ( 𝐴 𝐹 𝐵 ) = ( 𝐴 𝐺 𝐵 ) )