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 ˙ = K B × B
Assertion trleile K Toset X B Y B X ˙ Y Y ˙ X

Proof

Step Hyp Ref Expression
1 trleile.b B = Base K
2 trleile.l ˙ = K B × B
3 eqid K = K
4 1 3 tleile K Toset X B Y B X K Y Y K X
5 3simpc K Toset X B Y B X B Y B
6 brxp X B × B Y X B Y B
7 5 6 sylibr K Toset X B Y B X B × B Y
8 brin X K B × B Y X K Y X B × B Y
9 8 rbaib X B × B Y X K B × B Y X K Y
10 7 9 syl K Toset X B Y B X K B × B Y X K Y
11 5 ancomd K Toset X B Y B Y B X B
12 brxp Y B × B X Y B X B
13 11 12 sylibr K Toset X B Y B Y B × B X
14 brin Y K B × B X Y K X Y B × B X
15 14 rbaib Y B × B X Y K B × B X Y K X
16 13 15 syl K Toset X B Y B Y K B × B X Y K X
17 10 16 orbi12d K Toset X B Y B X K B × B Y Y K B × B X X K Y Y K X
18 4 17 mpbird K Toset X B Y B X K B × B Y Y K B × B X
19 2 breqi X ˙ Y X K B × B Y
20 2 breqi Y ˙ X Y K B × B X
21 19 20 orbi12i X ˙ Y Y ˙ X X K B × B Y Y K B × B X
22 18 21 sylibr K Toset X B Y B X ˙ Y Y ˙ X