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

Metamath Proof Explorer

Theorem elreldm

Description: The first member of an ordered pair in a relation belongs to the domain of the relation (see op1stb ). (Contributed by NM, 28-Jul-2004)

Ref Expression
Assertion elreldm ( ( Rel 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ∩ ∩ 𝐵 ∈ dom 𝐴 )

Proof

Step Hyp Ref Expression
1 df-rel ⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
2 ssel ⊢ ( 𝐴 ⊆ ( V × V ) → ( 𝐵 ∈ 𝐴 → 𝐵 ∈ ( V × V ) ) )
3 1 2 sylbi ⊢ ( Rel 𝐴 → ( 𝐵 ∈ 𝐴 → 𝐵 ∈ ( V × V ) ) )
4 elvv ⊢ ( 𝐵 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ )
5 3 4 imbitrdi ⊢ ( Rel 𝐴 → ( 𝐵 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ) )
6 eleq1 ⊢ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐵 ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
7 vex ⊢ 𝑥 ∈ V
8 vex ⊢ 𝑦 ∈ V
9 7 8 opeldm ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴 )
10 6 9 biimtrdi ⊢ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐵 ∈ 𝐴 → 𝑥 ∈ dom 𝐴 ) )
11 inteq ⊢ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ → ∩ 𝐵 = ∩ ⟨ 𝑥 , 𝑦 ⟩ )
12 11 inteqd ⊢ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ → ∩ ∩ 𝐵 = ∩ ∩ ⟨ 𝑥 , 𝑦 ⟩ )
13 7 8 op1stb ⊢ ∩ ∩ ⟨ 𝑥 , 𝑦 ⟩ = 𝑥
14 12 13 eqtrdi ⊢ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ → ∩ ∩ 𝐵 = 𝑥 )
15 14 eleq1d ⊢ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∩ ∩ 𝐵 ∈ dom 𝐴 ↔ 𝑥 ∈ dom 𝐴 ) )
16 10 15 sylibrd ⊢ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐵 ∈ 𝐴 → ∩ ∩ 𝐵 ∈ dom 𝐴 ) )
17 16 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐵 ∈ 𝐴 → ∩ ∩ 𝐵 ∈ dom 𝐴 ) )
18 5 17 syli ⊢ ( Rel 𝐴 → ( 𝐵 ∈ 𝐴 → ∩ ∩ 𝐵 ∈ dom 𝐴 ) )
19 18 imp ⊢ ( ( Rel 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ∩ ∩ 𝐵 ∈ dom 𝐴 )