Metamath Proof Explorer

Theorem ordthauslem

Description: Lemma for ordthaus . (Contributed by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypothesis ordthauslem.1 ⊢ 𝑋 = dom 𝑅
Assertion ordthauslem ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑅 𝐵 → ( 𝐴 ≠ 𝐵 → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )

Proof

Step Hyp Ref Expression
1 ordthauslem.1 ⊢ 𝑋 = dom 𝑅
2 simpll1 ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ ) → 𝑅 ∈ TosetRel )
3 simpll3 ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ ) → 𝐵 ∈ 𝑋 )
4 1 ordtopn2 ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝐵 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∈ ( ordTop ‘ 𝑅 ) )
5 2 3 4 syl2anc ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∈ ( ordTop ‘ 𝑅 ) )
6 simpll2 ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ ) → 𝐴 ∈ 𝑋 )
7 1 ordtopn1 ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } ∈ ( ordTop ‘ 𝑅 ) )
8 2 6 7 syl2anc ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } ∈ ( ordTop ‘ 𝑅 ) )
9 breq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐵 𝑅 𝑥 ↔ 𝐵 𝑅 𝐴 ) )
10 9 notbid ⊢ ( 𝑥 = 𝐴 → ( ¬ 𝐵 𝑅 𝑥 ↔ ¬ 𝐵 𝑅 𝐴 ) )
11 simprr ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) → 𝐴 ≠ 𝐵 )
12 simpl1 ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) → 𝑅 ∈ TosetRel )
13 tsrps ⊢ ( 𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel )
14 12 13 syl ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) → 𝑅 ∈ PosetRel )
15 simprl ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) → 𝐴 𝑅 𝐵 )
16 psasym ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) → 𝐴 = 𝐵 )
17 16 3expia ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 𝑅 𝐵 ) → ( 𝐵 𝑅 𝐴 → 𝐴 = 𝐵 ) )
18 14 15 17 syl2anc ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐵 𝑅 𝐴 → 𝐴 = 𝐵 ) )
19 18 necon3ad ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 ≠ 𝐵 → ¬ 𝐵 𝑅 𝐴 ) )
20 11 19 mpd ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) → ¬ 𝐵 𝑅 𝐴 )
21 20 adantr ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ ) → ¬ 𝐵 𝑅 𝐴 )
22 10 6 21 elrabd ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ ) → 𝐴 ∈ { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } )
23 breq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 𝑅 𝐴 ↔ 𝐵 𝑅 𝐴 ) )
24 23 notbid ⊢ ( 𝑥 = 𝐵 → ( ¬ 𝑥 𝑅 𝐴 ↔ ¬ 𝐵 𝑅 𝐴 ) )
25 24 3 21 elrabd ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ ) → 𝐵 ∈ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } )
26 simpr ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ ) → { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ )
27 eleq2 ⊢ ( 𝑚 = { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } → ( 𝐴 ∈ 𝑚 ↔ 𝐴 ∈ { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ) )
28 ineq1 ⊢ ( 𝑚 = { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } → ( 𝑚 ∩ 𝑛 ) = ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∩ 𝑛 ) )
29 28 eqeq1d ⊢ ( 𝑚 = { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } → ( ( 𝑚 ∩ 𝑛 ) = ∅ ↔ ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∩ 𝑛 ) = ∅ ) )
30 27 29 3anbi13d ⊢ ( 𝑚 = { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } → ( ( 𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ( 𝐴 ∈ { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∧ 𝐵 ∈ 𝑛 ∧ ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∩ 𝑛 ) = ∅ ) ) )
31 eleq2 ⊢ ( 𝑛 = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } → ( 𝐵 ∈ 𝑛 ↔ 𝐵 ∈ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } ) )
32 ineq2 ⊢ ( 𝑛 = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } → ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∩ 𝑛 ) = ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∩ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } ) )
33 inrab ⊢ ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∩ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } ) = { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) }
34 32 33 eqtrdi ⊢ ( 𝑛 = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } → ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∩ 𝑛 ) = { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } )
35 34 eqeq1d ⊢ ( 𝑛 = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } → ( ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∩ 𝑛 ) = ∅ ↔ { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ ) )
36 31 35 3anbi23d ⊢ ( 𝑛 = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } → ( ( 𝐴 ∈ { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∧ 𝐵 ∈ 𝑛 ∧ ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∩ 𝑛 ) = ∅ ) ↔ ( 𝐴 ∈ { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∧ 𝐵 ∈ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } ∧ { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ ) ) )
37 30 36 rspc2ev ⊢ ( ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∈ ( ordTop ‘ 𝑅 ) ∧ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } ∈ ( ordTop ‘ 𝑅 ) ∧ ( 𝐴 ∈ { 𝑥 ∈ 𝑋 ∣ ¬ 𝐵 𝑅 𝑥 } ∧ 𝐵 ∈ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝐴 } ∧ { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ ) ) → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
38 5 8 22 25 26 37 syl113anc ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ ) → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
39 38 ex ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) → ( { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } = ∅ → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
40 rabn0 ⊢ ( { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝑋 ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) )
41 simpll1 ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → 𝑅 ∈ TosetRel )
42 simprl ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → 𝑥 ∈ 𝑋 )
43 1 ordtopn2 ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋 ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∈ ( ordTop ‘ 𝑅 ) )
44 41 42 43 syl2anc ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∈ ( ordTop ‘ 𝑅 ) )
45 1 ordtopn1 ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋 ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ∈ ( ordTop ‘ 𝑅 ) )
46 41 42 45 syl2anc ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ∈ ( ordTop ‘ 𝑅 ) )
47 breq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝐴 ) )
48 47 notbid ⊢ ( 𝑦 = 𝐴 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑥 𝑅 𝐴 ) )
49 simpll2 ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → 𝐴 ∈ 𝑋 )
50 simprrr ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → ¬ 𝑥 𝑅 𝐴 )
51 48 49 50 elrabd ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → 𝐴 ∈ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
52 breq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 𝑅 𝑥 ↔ 𝐵 𝑅 𝑥 ) )
53 52 notbid ⊢ ( 𝑦 = 𝐵 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝐵 𝑅 𝑥 ) )
54 simpll3 ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → 𝐵 ∈ 𝑋 )
55 simprrl ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → ¬ 𝐵 𝑅 𝑥 )
56 53 54 55 elrabd ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → 𝐵 ∈ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
57 41 42 jca ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → ( 𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋 ) )
58 1 tsrlin ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
59 58 3expa ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
60 57 59 sylan ⊢ ( ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
61 oran ⊢ ( ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ¬ ( ¬ 𝑥 𝑅 𝑦 ∧ ¬ 𝑦 𝑅 𝑥 ) )
62 60 61 sylib ⊢ ( ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ¬ ( ¬ 𝑥 𝑅 𝑦 ∧ ¬ 𝑦 𝑅 𝑥 ) )
63 62 ralrimiva ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → ∀ 𝑦 ∈ 𝑋 ¬ ( ¬ 𝑥 𝑅 𝑦 ∧ ¬ 𝑦 𝑅 𝑥 ) )
64 rabeq0 ⊢ ( { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑥 𝑅 𝑦 ∧ ¬ 𝑦 𝑅 𝑥 ) } = ∅ ↔ ∀ 𝑦 ∈ 𝑋 ¬ ( ¬ 𝑥 𝑅 𝑦 ∧ ¬ 𝑦 𝑅 𝑥 ) )
65 63 64 sylibr ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑥 𝑅 𝑦 ∧ ¬ 𝑦 𝑅 𝑥 ) } = ∅ )
66 eleq2 ⊢ ( 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } → ( 𝐴 ∈ 𝑚 ↔ 𝐴 ∈ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
67 ineq1 ⊢ ( 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } → ( 𝑚 ∩ 𝑛 ) = ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∩ 𝑛 ) )
68 67 eqeq1d ⊢ ( 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } → ( ( 𝑚 ∩ 𝑛 ) = ∅ ↔ ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∩ 𝑛 ) = ∅ ) )
69 66 68 3anbi13d ⊢ ( 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } → ( ( 𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ( 𝐴 ∈ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∧ 𝐵 ∈ 𝑛 ∧ ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∩ 𝑛 ) = ∅ ) ) )
70 eleq2 ⊢ ( 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } → ( 𝐵 ∈ 𝑛 ↔ 𝐵 ∈ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
71 ineq2 ⊢ ( 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∩ 𝑛 ) = ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
72 inrab ⊢ ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑥 𝑅 𝑦 ∧ ¬ 𝑦 𝑅 𝑥 ) }
73 71 72 eqtrdi ⊢ ( 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∩ 𝑛 ) = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑥 𝑅 𝑦 ∧ ¬ 𝑦 𝑅 𝑥 ) } )
74 73 eqeq1d ⊢ ( 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } → ( ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∩ 𝑛 ) = ∅ ↔ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑥 𝑅 𝑦 ∧ ¬ 𝑦 𝑅 𝑥 ) } = ∅ ) )
75 70 74 3anbi23d ⊢ ( 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } → ( ( 𝐴 ∈ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∧ 𝐵 ∈ 𝑛 ∧ ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∩ 𝑛 ) = ∅ ) ↔ ( 𝐴 ∈ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∧ 𝐵 ∈ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ∧ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑥 𝑅 𝑦 ∧ ¬ 𝑦 𝑅 𝑥 ) } = ∅ ) ) )
76 69 75 rspc2ev ⊢ ( ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∈ ( ordTop ‘ 𝑅 ) ∧ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ∈ ( ordTop ‘ 𝑅 ) ∧ ( 𝐴 ∈ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∧ 𝐵 ∈ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ∧ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑥 𝑅 𝑦 ∧ ¬ 𝑦 𝑅 𝑥 ) } = ∅ ) ) → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
77 44 46 51 56 65 76 syl113anc ⊢ ( ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) ) ) → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
78 77 rexlimdvaa ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝑋 ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
79 40 78 biimtrid ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) → ( { 𝑥 ∈ 𝑋 ∣ ( ¬ 𝐵 𝑅 𝑥 ∧ ¬ 𝑥 𝑅 𝐴 ) } ≠ ∅ → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
80 39 79 pm2.61dne ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
81 80 exp32 ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑅 𝐵 → ( 𝐴 ≠ 𝐵 → ∃ 𝑚 ∈ ( ordTop ‘ 𝑅 ) ∃ 𝑛 ∈ ( ordTop ‘ 𝑅 ) ( 𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )