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

Metamath Proof Explorer

Theorem releldm2

Description: Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013)

Ref Expression
Assertion releldm2 ( Rel 𝐴 → ( 𝐵 ∈ dom 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐵 ∈ dom 𝐴 → 𝐵 ∈ V )
2 1 anim2i ⊢ ( ( Rel 𝐴 ∧ 𝐵 ∈ dom 𝐴 ) → ( Rel 𝐴 ∧ 𝐵 ∈ V ) )
3 id ⊢ ( ( 1st ‘ 𝑥 ) = 𝐵 → ( 1st ‘ 𝑥 ) = 𝐵 )
4 fvex ⊢ ( 1st ‘ 𝑥 ) ∈ V
5 3 4 eqeltrrdi ⊢ ( ( 1st ‘ 𝑥 ) = 𝐵 → 𝐵 ∈ V )
6 5 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 → 𝐵 ∈ V )
7 6 anim2i ⊢ ( ( Rel 𝐴 ∧ ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ) → ( Rel 𝐴 ∧ 𝐵 ∈ V ) )
8 eldm2g ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ dom 𝐴 ↔ ∃ 𝑦 ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐴 ) )
9 8 adantl ⊢ ( ( Rel 𝐴 ∧ 𝐵 ∈ V ) → ( 𝐵 ∈ dom 𝐴 ↔ ∃ 𝑦 ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐴 ) )
10 df-rel ⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
11 ssel ⊢ ( 𝐴 ⊆ ( V × V ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( V × V ) ) )
12 10 11 sylbi ⊢ ( Rel 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( V × V ) ) )
13 12 imp ⊢ ( ( Rel 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( V × V ) )
14 op1steq ⊢ ( 𝑥 ∈ ( V × V ) → ( ( 1st ‘ 𝑥 ) = 𝐵 ↔ ∃ 𝑦 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ ) )
15 13 14 syl ⊢ ( ( Rel 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 1st ‘ 𝑥 ) = 𝐵 ↔ ∃ 𝑦 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ ) )
16 15 rexbidva ⊢ ( Rel 𝐴 → ( ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ ) )
17 16 adantr ⊢ ( ( Rel 𝐴 ∧ 𝐵 ∈ V ) → ( ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ ) )
18 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ )
19 risset ⊢ ( ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ )
20 19 exbii ⊢ ( ∃ 𝑦 ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐴 ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ )
21 18 20 bitr4i ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ ↔ ∃ 𝑦 ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐴 )
22 17 21 bitrdi ⊢ ( ( Rel 𝐴 ∧ 𝐵 ∈ V ) → ( ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ↔ ∃ 𝑦 ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐴 ) )
23 9 22 bitr4d ⊢ ( ( Rel 𝐴 ∧ 𝐵 ∈ V ) → ( 𝐵 ∈ dom 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ) )
24 2 7 23 pm5.21nd ⊢ ( Rel 𝐴 → ( 𝐵 ∈ dom 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ) )