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 𝐴 )