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 ⁡ A ∧ B ∈ A → ⋂ ⋂ B ∈ dom ⁡ A

Proof

Step Hyp Ref Expression
1 df-rel ⊢ Rel ⁡ A ↔ A ⊆ V × V
2 ssel ⊢ A ⊆ V × V → B ∈ A → B ∈ V × V
3 1 2 sylbi ⊢ Rel ⁡ A → B ∈ A → B ∈ V × V
4 elvv ⊢ B ∈ V × V ↔ ∃ x ∃ y B = x y
5 3 4 imbitrdi ⊢ Rel ⁡ A → B ∈ A → ∃ x ∃ y B = x y
6 eleq1 ⊢ B = x y → B ∈ A ↔ x y ∈ A
7 vex ⊢ x ∈ V
8 vex ⊢ y ∈ V
9 7 8 opeldm ⊢ x y ∈ A → x ∈ dom ⁡ A
10 6 9 biimtrdi ⊢ B = x y → B ∈ A → x ∈ dom ⁡ A
11 inteq ⊢ B = x y → ⋂ B = ⋂ x y
12 11 inteqd ⊢ B = x y → ⋂ ⋂ B = ⋂ ⋂ x y
13 7 8 op1stb ⊢ ⋂ ⋂ x y = x
14 12 13 eqtrdi ⊢ B = x y → ⋂ ⋂ B = x
15 14 eleq1d ⊢ B = x y → ⋂ ⋂ B ∈ dom ⁡ A ↔ x ∈ dom ⁡ A
16 10 15 sylibrd ⊢ B = x y → B ∈ A → ⋂ ⋂ B ∈ dom ⁡ A
17 16 exlimivv ⊢ ∃ x ∃ y B = x y → B ∈ A → ⋂ ⋂ B ∈ dom ⁡ A
18 5 17 syli ⊢ Rel ⁡ A → B ∈ A → ⋂ ⋂ B ∈ dom ⁡ A
19 18 imp ⊢ Rel ⁡ A ∧ B ∈ A → ⋂ ⋂ B ∈ dom ⁡ A