# Metamath Proof Explorer

## Theorem swoord2

Description: The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014)

Ref Expression
Hypotheses swoer.1
swoer.2
swoer.3
swoord.4 ${⊢}{\phi }\to {B}\in {X}$
swoord.5 ${⊢}{\phi }\to {C}\in {X}$
swoord.6 ${⊢}{\phi }\to {A}{R}{B}$
Assertion swoord2

### Proof

Step Hyp Ref Expression
1 swoer.1
2 swoer.2
3 swoer.3
4 swoord.4 ${⊢}{\phi }\to {B}\in {X}$
5 swoord.5 ${⊢}{\phi }\to {C}\in {X}$
6 swoord.6 ${⊢}{\phi }\to {A}{R}{B}$
7 id ${⊢}{\phi }\to {\phi }$
8 difss
9 1 8 eqsstri ${⊢}{R}\subseteq {X}×{X}$
10 9 ssbri ${⊢}{A}{R}{B}\to {A}\left({X}×{X}\right){B}$
11 df-br ${⊢}{A}\left({X}×{X}\right){B}↔⟨{A},{B}⟩\in \left({X}×{X}\right)$
12 opelxp1 ${⊢}⟨{A},{B}⟩\in \left({X}×{X}\right)\to {A}\in {X}$
13 11 12 sylbi ${⊢}{A}\left({X}×{X}\right){B}\to {A}\in {X}$
14 6 10 13 3syl ${⊢}{\phi }\to {A}\in {X}$
15 3 swopolem
16 7 5 14 4 15 syl13anc
17 idd
18 1 brdifun
19 14 4 18 syl2anc
20 6 19 mpbid
21 olc
22 20 21 nsyl
23 22 pm2.21d
24 17 23 jaod
25 16 24 syld
26 3 swopolem
27 7 5 4 14 26 syl13anc
28 idd
29 orc
30 20 29 nsyl
31 30 pm2.21d
32 28 31 jaod
33 27 32 syld
34 25 33 impbid