Metamath Proof Explorer

Theorem prsdm

Description: Domain of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2015)

Ref Expression
Hypotheses ordtNEW.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ordtNEW.l ⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
Assertion prsdm ( 𝐾 ∈ Proset → dom ≤ = 𝐵 )

Proof

Step Hyp Ref Expression
1 ordtNEW.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ordtNEW.l ⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
3 2 dmeqi ⊢ dom ≤ = dom ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
4 3 eleq2i ⊢ ( 𝑥 ∈ dom ≤ ↔ 𝑥 ∈ dom ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) )
5 vex ⊢ 𝑥 ∈ V
6 5 eldm2 ⊢ ( 𝑥 ∈ dom ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) )
7 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
8 1 7 prsref ⊢ ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ( le ‘ 𝐾 ) 𝑥 )
9 df-br ⊢ ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ↔ ⟨ 𝑥 , 𝑥 ⟩ ∈ ( le ‘ 𝐾 ) )
10 8 9 sylib ⊢ ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑥 ⟩ ∈ ( le ‘ 𝐾 ) )
11 simpr ⊢ ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
12 11 11 opelxpd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑥 ⟩ ∈ ( 𝐵 × 𝐵 ) )
13 10 12 elind ⊢ ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑥 ⟩ ∈ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) )
14 opeq2 ⊢ ( 𝑦 = 𝑥 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑥 ⟩ )
15 14 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) ↔ ⟨ 𝑥 , 𝑥 ⟩ ∈ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) ) )
16 5 15 spcev ⊢ ( ⟨ 𝑥 , 𝑥 ⟩ ∈ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) → ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) )
17 13 16 syl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) )
18 17 ex ⊢ ( 𝐾 ∈ Proset → ( 𝑥 ∈ 𝐵 → ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) ) )
19 elinel2 ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) )
20 opelxp1 ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) → 𝑥 ∈ 𝐵 )
21 19 20 syl ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) → 𝑥 ∈ 𝐵 )
22 21 exlimiv ⊢ ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) → 𝑥 ∈ 𝐵 )
23 18 22 impbid1 ⊢ ( 𝐾 ∈ Proset → ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) ) )
24 6 23 bitr4id ⊢ ( 𝐾 ∈ Proset → ( 𝑥 ∈ dom ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) ↔ 𝑥 ∈ 𝐵 ) )
25 4 24 bitrid ⊢ ( 𝐾 ∈ Proset → ( 𝑥 ∈ dom ≤ ↔ 𝑥 ∈ 𝐵 ) )
26 25 eqrdv ⊢ ( 𝐾 ∈ Proset → dom ≤ = 𝐵 )