Metamath Proof Explorer

Theorem prsrn

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

Ref Expression
Hypotheses ordtNEW.b 
|- B = ( Base ` K )
ordtNEW.l 
|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
Assertion prsrn 
|- ( K e. Proset -> ran .<_ = B )

Proof

Step Hyp Ref Expression
1 ordtNEW.b 
 |-  B = ( Base ` K )
2 ordtNEW.l 
 |-  .<_ = ( ( le ` K ) i^i ( B X. B ) )
3 2 rneqi 
 |-  ran .<_ = ran ( ( le ` K ) i^i ( B X. B ) )
4 3 eleq2i 
 |-  ( x e. ran .<_ <-> x e. ran ( ( le ` K ) i^i ( B X. B ) ) )
5 vex 
 |-  x e. _V
6 5 elrn2 
 |-  ( x e. ran ( ( le ` K ) i^i ( B X. B ) ) <-> E. y <. y , x >. 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 opeq1 
 |-  ( y = x -> <. y , x >. = <. x , x >. )
15 14 eleq1d 
 |-  ( y = x -> ( <. y , x >. 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 <. y , x >. e. ( ( le ` K ) i^i ( B X. B ) ) )
17 13 16 syl 
 |-  ( ( K e. Proset /\ x e. B ) -> E. y <. y , x >. e. ( ( le ` K ) i^i ( B X. B ) ) )
18 17 ex 
 |-  ( K e. Proset -> ( x e. B -> E. y <. y , x >. e. ( ( le ` K ) i^i ( B X. B ) ) ) )
19 elinel2 
 |-  ( <. y , x >. e. ( ( le ` K ) i^i ( B X. B ) ) -> <. y , x >. e. ( B X. B ) )
20 opelxp2 
 |-  ( <. y , x >. e. ( B X. B ) -> x e. B )
21 19 20 syl 
 |-  ( <. y , x >. e. ( ( le ` K ) i^i ( B X. B ) ) -> x e. B )
22 21 exlimiv 
 |-  ( E. y <. y , x >. e. ( ( le ` K ) i^i ( B X. B ) ) -> x e. B )
23 18 22 impbid1 
 |-  ( K e. Proset -> ( x e. B <-> E. y <. y , x >. e. ( ( le ` K ) i^i ( B X. B ) ) ) )
24 6 23 bitr4id 
 |-  ( K e. Proset -> ( x e. ran ( ( le ` K ) i^i ( B X. B ) ) <-> x e. B ) )
25 4 24 syl5bb 
 |-  ( K e. Proset -> ( x e. ran .<_ <-> x e. B ) )
26 25 eqrdv 
 |-  ( K e. Proset -> ran .<_ = B )