Theorem swoer

Description: Incomparability under a strict weak partial order is an equivalence relation. (Contributed by Mario Carneiro, 9-Jul-2014) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypotheses	swoer.1	⊢ 𝑅 = ( ( 𝑋 × 𝑋 ) ∖ ( < ∪ ◡ < ) )
	swoer.2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 < 𝑧 → ¬ 𝑧 < 𝑦 ) )
	swoer.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 < 𝑦 → ( 𝑥 < 𝑧 ∨ 𝑧 < 𝑦 ) ) )
Assertion	swoer	⊢ ( 𝜑 → 𝑅 Er 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		swoer.1	⊢ 𝑅 = ( ( 𝑋 × 𝑋 ) ∖ ( < ∪ ◡ < ) )
2		swoer.2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 < 𝑧 → ¬ 𝑧 < 𝑦 ) )
3		swoer.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 < 𝑦 → ( 𝑥 < 𝑧 ∨ 𝑧 < 𝑦 ) ) )
4		difss	⊢ ( ( 𝑋 × 𝑋 ) ∖ ( < ∪ ◡ < ) ) ⊆ ( 𝑋 × 𝑋 )
5	1 4	eqsstri	⊢ 𝑅 ⊆ ( 𝑋 × 𝑋 )
6		relxp	⊢ Rel ( 𝑋 × 𝑋 )
7		relss	⊢ ( 𝑅 ⊆ ( 𝑋 × 𝑋 ) → ( Rel ( 𝑋 × 𝑋 ) → Rel 𝑅 ) )
8	5 6 7	mp2	⊢ Rel 𝑅
9	8	a1i	⊢ ( 𝜑 → Rel 𝑅 )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → 𝑢 𝑅 𝑣 )
11		orcom	⊢ ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ↔ ( 𝑣 < 𝑢 ∨ 𝑢 < 𝑣 ) )
12	11	a1i	⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ↔ ( 𝑣 < 𝑢 ∨ 𝑢 < 𝑣 ) ) )
13	12	notbid	⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → ( ¬ ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ↔ ¬ ( 𝑣 < 𝑢 ∨ 𝑢 < 𝑣 ) ) )
14	5	ssbri	⊢ ( 𝑢 𝑅 𝑣 → 𝑢 ( 𝑋 × 𝑋 ) 𝑣 )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → 𝑢 ( 𝑋 × 𝑋 ) 𝑣 )
16		brxp	⊢ ( 𝑢 ( 𝑋 × 𝑋 ) 𝑣 ↔ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) )
17	15 16	sylib	⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) )
18	1	brdifun	⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) → ( 𝑢 𝑅 𝑣 ↔ ¬ ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ) )
19	17 18	syl	⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → ( 𝑢 𝑅 𝑣 ↔ ¬ ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ) )
20	17	simprd	⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → 𝑣 ∈ 𝑋 )
21	17	simpld	⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → 𝑢 ∈ 𝑋 )
22	1	brdifun	⊢ ( ( 𝑣 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) → ( 𝑣 𝑅 𝑢 ↔ ¬ ( 𝑣 < 𝑢 ∨ 𝑢 < 𝑣 ) ) )
23	20 21 22	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → ( 𝑣 𝑅 𝑢 ↔ ¬ ( 𝑣 < 𝑢 ∨ 𝑢 < 𝑣 ) ) )
24	13 19 23	3bitr4d	⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → ( 𝑢 𝑅 𝑣 ↔ 𝑣 𝑅 𝑢 ) )
25	10 24	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → 𝑣 𝑅 𝑢 )
26		simprl	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑢 𝑅 𝑣 )
27	14	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑢 ( 𝑋 × 𝑋 ) 𝑣 )
28	16	simplbi	⊢ ( 𝑢 ( 𝑋 × 𝑋 ) 𝑣 → 𝑢 ∈ 𝑋 )
29	27 28	syl	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑢 ∈ 𝑋 )
30	16	simprbi	⊢ ( 𝑢 ( 𝑋 × 𝑋 ) 𝑣 → 𝑣 ∈ 𝑋 )
31	27 30	syl	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑣 ∈ 𝑋 )
32	29 31 18	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( 𝑢 𝑅 𝑣 ↔ ¬ ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ) )
33	26 32	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ¬ ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) )
34		simprr	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑣 𝑅 𝑤 )
35	5	brel	⊢ ( 𝑣 𝑅 𝑤 → ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) )
36	35	simprd	⊢ ( 𝑣 𝑅 𝑤 → 𝑤 ∈ 𝑋 )
37	34 36	syl	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑤 ∈ 𝑋 )
38	1	brdifun	⊢ ( ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑣 𝑅 𝑤 ↔ ¬ ( 𝑣 < 𝑤 ∨ 𝑤 < 𝑣 ) ) )
39	31 37 38	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( 𝑣 𝑅 𝑤 ↔ ¬ ( 𝑣 < 𝑤 ∨ 𝑤 < 𝑣 ) ) )
40	34 39	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ¬ ( 𝑣 < 𝑤 ∨ 𝑤 < 𝑣 ) )
41		simpl	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝜑 )
42	3	swopolem	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) → ( 𝑢 < 𝑤 → ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑤 ) ) )
43	41 29 37 31 42	syl13anc	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( 𝑢 < 𝑤 → ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑤 ) ) )
44	3	swopolem	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) → ( 𝑤 < 𝑢 → ( 𝑤 < 𝑣 ∨ 𝑣 < 𝑢 ) ) )
45	41 37 29 31 44	syl13anc	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( 𝑤 < 𝑢 → ( 𝑤 < 𝑣 ∨ 𝑣 < 𝑢 ) ) )
46		orcom	⊢ ( ( 𝑣 < 𝑢 ∨ 𝑤 < 𝑣 ) ↔ ( 𝑤 < 𝑣 ∨ 𝑣 < 𝑢 ) )
47	45 46	imbitrrdi	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( 𝑤 < 𝑢 → ( 𝑣 < 𝑢 ∨ 𝑤 < 𝑣 ) ) )
48	43 47	orim12d	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( ( 𝑢 < 𝑤 ∨ 𝑤 < 𝑢 ) → ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑤 ) ∨ ( 𝑣 < 𝑢 ∨ 𝑤 < 𝑣 ) ) ) )
49		or4	⊢ ( ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑤 ) ∨ ( 𝑣 < 𝑢 ∨ 𝑤 < 𝑣 ) ) ↔ ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ∨ ( 𝑣 < 𝑤 ∨ 𝑤 < 𝑣 ) ) )
50	48 49	imbitrdi	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( ( 𝑢 < 𝑤 ∨ 𝑤 < 𝑢 ) → ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ∨ ( 𝑣 < 𝑤 ∨ 𝑤 < 𝑣 ) ) ) )
51	33 40 50	mtord	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ¬ ( 𝑢 < 𝑤 ∨ 𝑤 < 𝑢 ) )
52	1	brdifun	⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑢 𝑅 𝑤 ↔ ¬ ( 𝑢 < 𝑤 ∨ 𝑤 < 𝑢 ) ) )
53	29 37 52	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( 𝑢 𝑅 𝑤 ↔ ¬ ( 𝑢 < 𝑤 ∨ 𝑤 < 𝑢 ) ) )
54	51 53	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑢 𝑅 𝑤 )
55	2 3	swopo	⊢ ( 𝜑 → < Po 𝑋 )
56		poirr	⊢ ( ( < Po 𝑋 ∧ 𝑢 ∈ 𝑋 ) → ¬ 𝑢 < 𝑢 )
57	55 56	sylan	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → ¬ 𝑢 < 𝑢 )
58		pm1.2	⊢ ( ( 𝑢 < 𝑢 ∨ 𝑢 < 𝑢 ) → 𝑢 < 𝑢 )
59	57 58	nsyl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → ¬ ( 𝑢 < 𝑢 ∨ 𝑢 < 𝑢 ) )
60		simpr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → 𝑢 ∈ 𝑋 )
61	1	brdifun	⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 𝑅 𝑢 ↔ ¬ ( 𝑢 < 𝑢 ∨ 𝑢 < 𝑢 ) ) )
62	60 60 61	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 𝑅 𝑢 ↔ ¬ ( 𝑢 < 𝑢 ∨ 𝑢 < 𝑢 ) ) )
63	59 62	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → 𝑢 𝑅 𝑢 )
64	5	ssbri	⊢ ( 𝑢 𝑅 𝑢 → 𝑢 ( 𝑋 × 𝑋 ) 𝑢 )
65		brxp	⊢ ( 𝑢 ( 𝑋 × 𝑋 ) 𝑢 ↔ ( 𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) )
66	65	simplbi	⊢ ( 𝑢 ( 𝑋 × 𝑋 ) 𝑢 → 𝑢 ∈ 𝑋 )
67	64 66	syl	⊢ ( 𝑢 𝑅 𝑢 → 𝑢 ∈ 𝑋 )
68	67	adantl	⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑢 ) → 𝑢 ∈ 𝑋 )
69	63 68	impbida	⊢ ( 𝜑 → ( 𝑢 ∈ 𝑋 ↔ 𝑢 𝑅 𝑢 ) )
70	9 25 54 69	iserd	⊢ ( 𝜑 → 𝑅 Er 𝑋 )