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

Metamath Proof Explorer

Theorem 2elresin

Description: Membership in two functions restricted by each other's domain. (Contributed by NM, 8-Aug-1994)

Ref Expression
Assertion 2elresin ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fnop ⊢ ( ( 𝐹 Fn 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → 𝑥 ∈ 𝐴 )
2 fnop ⊢ ( ( 𝐺 Fn 𝐵 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) → 𝑥 ∈ 𝐵 )
3 1 2 anim12i ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ∧ ( 𝐺 Fn 𝐵 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
4 3 an4s ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
5 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
6 4 5 sylibr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) → 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
7 vex ⊢ 𝑦 ∈ V
8 7 opres ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
9 vex ⊢ 𝑧 ∈ V
10 9 opres ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) )
11 8 10 anbi12d ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) )
12 11 biimprd ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) ) )
13 6 12 syl ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) ) )
14 13 ex ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) ) ) )
15 14 pm2.43d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) ) )
16 resss ⊢ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐹
17 16 sseli ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
18 resss ⊢ ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐺
19 18 sseli ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 )
20 17 19 anim12i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) )
21 15 20 impbid1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) ) )