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
|- B = ( Base ` K )
ordtNEW.l
|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
Assertion prsdm
|- ( K e. Proset -> dom .<_ = B )

Proof

Step Hyp Ref Expression
1 ordtNEW.b
 |-  B = ( Base ` K )
2 ordtNEW.l
 |-  .<_ = ( ( le ` K ) i^i ( B X. B ) )
3 2 dmeqi
 |-  dom .<_ = dom ( ( le ` K ) i^i ( B X. B ) )
4 3 eleq2i
 |-  ( x e. dom .<_ <-> x e. dom ( ( le ` K ) i^i ( B X. B ) ) )
5 vex
 |-  x e. _V
6 5 eldm2
 |-  ( x e. dom ( ( le ` K ) i^i ( B X. B ) ) <-> E. y <. x , y >. e. ( ( le ` K ) i^i ( B X. B ) ) )
7 eqid
 |-  ( le ` K ) = ( le ` K )
8 1 7 prsref
 |-  ( ( K e. Proset /\ x e. B ) -> x ( le ` K ) x )
9 df-br
 |-  ( x ( le ` K ) x <-> <. x , x >. e. ( le ` K ) )
10 8 9 sylib
 |-  ( ( K e. Proset /\ x e. B ) -> <. x , x >. e. ( le ` K ) )
11 simpr
 |-  ( ( K e. Proset /\ x e. B ) -> x e. B )
12 11 11 opelxpd
 |-  ( ( K e. Proset /\ x e. B ) -> <. x , x >. e. ( B X. B ) )
13 10 12 elind
 |-  ( ( K e. Proset /\ x e. B ) -> <. x , x >. e. ( ( le ` K ) i^i ( B X. B ) ) )
14 opeq2
 |-  ( y = x -> <. x , y >. = <. x , x >. )
15 14 eleq1d
 |-  ( y = x -> ( <. x , y >. e. ( ( le ` K ) i^i ( B X. B ) ) <-> <. x , x >. e. ( ( le ` K ) i^i ( B X. B ) ) ) )
16 5 15 spcev
 |-  ( <. x , x >. e. ( ( le ` K ) i^i ( B X. B ) ) -> E. y <. x , y >. e. ( ( le ` K ) i^i ( B X. B ) ) )
17 13 16 syl
 |-  ( ( K e. Proset /\ x e. B ) -> E. y <. x , y >. e. ( ( le ` K ) i^i ( B X. B ) ) )
18 17 ex
 |-  ( K e. Proset -> ( x e. B -> E. y <. x , y >. e. ( ( le ` K ) i^i ( B X. B ) ) ) )
19 elinel2
 |-  ( <. x , y >. e. ( ( le ` K ) i^i ( B X. B ) ) -> <. x , y >. e. ( B X. B ) )
20 opelxp1
 |-  ( <. x , y >. e. ( B X. B ) -> x e. B )
21 19 20 syl
 |-  ( <. x , y >. e. ( ( le ` K ) i^i ( B X. B ) ) -> x e. B )
22 21 exlimiv
 |-  ( E. y <. x , y >. e. ( ( le ` K ) i^i ( B X. B ) ) -> x e. B )
23 18 22 impbid1
 |-  ( K e. Proset -> ( x e. B <-> E. y <. x , y >. e. ( ( le ` K ) i^i ( B X. B ) ) ) )
24 6 23 bitr4id
 |-  ( K e. Proset -> ( x e. dom ( ( le ` K ) i^i ( B X. B ) ) <-> x e. B ) )
25 4 24 syl5bb
 |-  ( K e. Proset -> ( x e. dom .<_ <-> x e. B ) )
26 25 eqrdv
 |-  ( K e. Proset -> dom .<_ = B )