Metamath Proof Explorer

Theorem posrasymb

Description: A poset ordering is asymetric. (Contributed by Thierry Arnoux, 13-Sep-2018)

Ref Expression
Hypotheses posrasymb.b 
|- B = ( Base ` K )
posrasymb.l 
|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
Assertion posrasymb 
|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( ( X .<_ Y /\ Y .<_ X ) <-> X = Y ) )

Proof

Step Hyp Ref Expression
1 posrasymb.b 
 |-  B = ( Base ` K )
2 posrasymb.l 
 |-  .<_ = ( ( le ` K ) i^i ( B X. B ) )
3 2 breqi 
 |-  ( X .<_ Y <-> X ( ( le ` K ) i^i ( B X. B ) ) Y )
4 simp2 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> X e. B )
5 simp3 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> Y e. B )
6 brxp 
 |-  ( X ( B X. B ) Y <-> ( X e. B /\ Y e. B ) )
7 4 5 6 sylanbrc 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> X ( B X. B ) Y )
8 brin 
 |-  ( X ( ( le ` K ) i^i ( B X. B ) ) Y <-> ( X ( le ` K ) Y /\ X ( B X. B ) Y ) )
9 8 rbaib 
 |-  ( X ( B X. B ) Y -> ( X ( ( le ` K ) i^i ( B X. B ) ) Y <-> X ( le ` K ) Y ) )
10 7 9 syl 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X ( ( le ` K ) i^i ( B X. B ) ) Y <-> X ( le ` K ) Y ) )
11 3 10 syl5bb 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> X ( le ` K ) Y ) )
12 2 breqi 
 |-  ( Y .<_ X <-> Y ( ( le ` K ) i^i ( B X. B ) ) X )
13 brxp 
 |-  ( Y ( B X. B ) X <-> ( Y e. B /\ X e. B ) )
14 5 4 13 sylanbrc 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> Y ( B X. B ) X )
15 brin 
 |-  ( Y ( ( le ` K ) i^i ( B X. B ) ) X <-> ( Y ( le ` K ) X /\ Y ( B X. B ) X ) )
16 15 rbaib 
 |-  ( Y ( B X. B ) X -> ( Y ( ( le ` K ) i^i ( B X. B ) ) X <-> Y ( le ` K ) X ) )
17 14 16 syl 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( Y ( ( le ` K ) i^i ( B X. B ) ) X <-> Y ( le ` K ) X ) )
18 12 17 syl5bb 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( Y .<_ X <-> Y ( le ` K ) X ) )
19 11 18 anbi12d 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( ( X .<_ Y /\ Y .<_ X ) <-> ( X ( le ` K ) Y /\ Y ( le ` K ) X ) ) )
20 eqid 
 |-  ( le ` K ) = ( le ` K )
21 1 20 posasymb 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( ( X ( le ` K ) Y /\ Y ( le ` K ) X ) <-> X = Y ) )
22 19 21 bitrd 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( ( X .<_ Y /\ Y .<_ X ) <-> X = Y ) )