Metamath Proof Explorer

Theorem trleile

Description: In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 12-Sep-2018)

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

Proof

Step Hyp Ref Expression
1 trleile.b 
 |-  B = ( Base ` K )
2 trleile.l 
 |-  .<_ = ( ( le ` K ) i^i ( B X. B ) )
3 eqid 
 |-  ( le ` K ) = ( le ` K )
4 1 3 tleile 
 |-  ( ( K e. Toset /\ X e. B /\ Y e. B ) -> ( X ( le ` K ) Y \/ Y ( le ` K ) X ) )
5 3simpc 
 |-  ( ( K e. Toset /\ X e. B /\ Y e. B ) -> ( X e. B /\ Y e. B ) )
6 brxp 
 |-  ( X ( B X. B ) Y <-> ( X e. B /\ Y e. B ) )
7 5 6 sylibr 
 |-  ( ( K e. Toset /\ 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. Toset /\ X e. B /\ Y e. B ) -> ( X ( ( le ` K ) i^i ( B X. B ) ) Y <-> X ( le ` K ) Y ) )
11 5 ancomd 
 |-  ( ( K e. Toset /\ X e. B /\ Y e. B ) -> ( Y e. B /\ X e. B ) )
12 brxp 
 |-  ( Y ( B X. B ) X <-> ( Y e. B /\ X e. B ) )
13 11 12 sylibr 
 |-  ( ( K e. Toset /\ X e. B /\ Y e. B ) -> Y ( B X. B ) X )
14 brin 
 |-  ( Y ( ( le ` K ) i^i ( B X. B ) ) X <-> ( Y ( le ` K ) X /\ Y ( B X. B ) X ) )
15 14 rbaib 
 |-  ( Y ( B X. B ) X -> ( Y ( ( le ` K ) i^i ( B X. B ) ) X <-> Y ( le ` K ) X ) )
16 13 15 syl 
 |-  ( ( K e. Toset /\ X e. B /\ Y e. B ) -> ( Y ( ( le ` K ) i^i ( B X. B ) ) X <-> Y ( le ` K ) X ) )
17 10 16 orbi12d 
 |-  ( ( K e. Toset /\ X e. B /\ Y e. B ) -> ( ( X ( ( le ` K ) i^i ( B X. B ) ) Y \/ Y ( ( le ` K ) i^i ( B X. B ) ) X ) <-> ( X ( le ` K ) Y \/ Y ( le ` K ) X ) ) )
18 4 17 mpbird 
 |-  ( ( K e. Toset /\ X e. B /\ Y e. B ) -> ( X ( ( le ` K ) i^i ( B X. B ) ) Y \/ Y ( ( le ` K ) i^i ( B X. B ) ) X ) )
19 2 breqi 
 |-  ( X .<_ Y <-> X ( ( le ` K ) i^i ( B X. B ) ) Y )
20 2 breqi 
 |-  ( Y .<_ X <-> Y ( ( le ` K ) i^i ( B X. B ) ) X )
21 19 20 orbi12i 
 |-  ( ( X .<_ Y \/ Y .<_ X ) <-> ( X ( ( le ` K ) i^i ( B X. B ) ) Y \/ Y ( ( le ` K ) i^i ( B X. B ) ) X ) )
22 18 21 sylibr 
 |-  ( ( K e. Toset /\ X e. B /\ Y e. B ) -> ( X .<_ Y \/ Y .<_ X ) )