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 )