Theorem swoso

Description: If the incomparability relation is equivalent to equality in a subset, then the partial order strictly orders the subset. (Contributed by Mario Carneiro, 30-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		swoer.1	⊢ 𝑅 = ( ( 𝑋 × 𝑋 ) ∖ ( < ∪ ◡ < ) )
2		swoer.2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 < 𝑧 → ¬ 𝑧 < 𝑦 ) )
3		swoer.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 < 𝑦 → ( 𝑥 < 𝑧 ∨ 𝑧 < 𝑦 ) ) )
4		swoso.4	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
5		swoso.5	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ∧ 𝑥 𝑅 𝑦 ) ) → 𝑥 = 𝑦 )
6	2 3	swopo	⊢ ( 𝜑 → < Po 𝑋 )
7		poss	⊢ ( 𝑌 ⊆ 𝑋 → ( < Po 𝑋 → < Po 𝑌 ) )
8	4 6 7	sylc	⊢ ( 𝜑 → < Po 𝑌 )
9	4	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 )
10	4	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑋 )
11	9 10	anim12dan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) )
12	1	brdifun	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑅 𝑦 ↔ ¬ ( 𝑥 < 𝑦 ∨ 𝑦 < 𝑥 ) ) )
13	11 12	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝑅 𝑦 ↔ ¬ ( 𝑥 < 𝑦 ∨ 𝑦 < 𝑥 ) ) )
14		df-3an	⊢ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ∧ 𝑥 𝑅 𝑦 ) ↔ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 𝑅 𝑦 ) )
15	14 5	sylan2br	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 𝑅 𝑦 ) ) → 𝑥 = 𝑦 )
16	15	expr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) )
17	13 16	sylbird	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( ¬ ( 𝑥 < 𝑦 ∨ 𝑦 < 𝑥 ) → 𝑥 = 𝑦 ) )
18	17	orrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( ( 𝑥 < 𝑦 ∨ 𝑦 < 𝑥 ) ∨ 𝑥 = 𝑦 ) )
19		3orcomb	⊢ ( ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥 ) ↔ ( 𝑥 < 𝑦 ∨ 𝑦 < 𝑥 ∨ 𝑥 = 𝑦 ) )
20		df-3or	⊢ ( ( 𝑥 < 𝑦 ∨ 𝑦 < 𝑥 ∨ 𝑥 = 𝑦 ) ↔ ( ( 𝑥 < 𝑦 ∨ 𝑦 < 𝑥 ) ∨ 𝑥 = 𝑦 ) )
21	19 20	bitri	⊢ ( ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥 ) ↔ ( ( 𝑥 < 𝑦 ∨ 𝑦 < 𝑥 ) ∨ 𝑥 = 𝑦 ) )
22	18 21	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥 ) )
23	8 22	issod	⊢ ( 𝜑 → < Or 𝑌 )