MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordthauslem Structured version   Visualization version   GIF version
Theorem ordthauslem 23300
Description: Lemma for ordthaus 23301. (Contributed by Mario Carneiro, 13-Sep-2015.)
Hypothesis
Ref Expression
ordthauslem.1 𝑋 = dom 𝑅
Assertion
Ref Expression
ordthauslem ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) β†’ (𝐴𝑅𝐡 β†’ (𝐴 β‰  𝐡 β†’ βˆƒπ‘š ∈ (ordTopβ€˜π‘…)βˆƒπ‘› ∈ (ordTopβ€˜π‘…)(𝐴 ∈ π‘š ∧ 𝐡 ∈ 𝑛 ∧ (π‘š ∩ 𝑛) = βˆ…))))
Distinct variable groups:   π‘š,𝑛,𝐴   𝐡,π‘š,𝑛   𝑅,π‘š,𝑛   π‘š,𝑋,𝑛
Proof of Theorem ordthauslem
Dummy variables π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll1 1209 . . . . . 6 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…) β†’ 𝑅 ∈ TosetRel )
2 simpll3 1211 . . . . . 6 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…) β†’ 𝐡 ∈ 𝑋)
3 ordthauslem.1 . . . . . . 7 𝑋 = dom 𝑅
43ordtopn2 23112 . . . . . 6 ((𝑅 ∈ TosetRel ∧ 𝐡 ∈ 𝑋) β†’ {π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∈ (ordTopβ€˜π‘…))
51, 2, 4syl2anc 582 . . . . 5 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…) β†’ {π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∈ (ordTopβ€˜π‘…))
6 simpll2 1210 . . . . . 6 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…) β†’ 𝐴 ∈ 𝑋)
73ordtopn1 23111 . . . . . 6 ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋) β†’ {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴} ∈ (ordTopβ€˜π‘…))
81, 6, 7syl2anc 582 . . . . 5 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…) β†’ {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴} ∈ (ordTopβ€˜π‘…))
9 breq2 5148 . . . . . . 7 (π‘₯ = 𝐴 β†’ (𝐡𝑅π‘₯ ↔ 𝐡𝑅𝐴))
109notbid 317 . . . . . 6 (π‘₯ = 𝐴 β†’ (Β¬ 𝐡𝑅π‘₯ ↔ Β¬ 𝐡𝑅𝐴))
11 simprr 771 . . . . . . . 8 (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) β†’ 𝐴 β‰  𝐡)
12 simpl1 1188 . . . . . . . . . . 11 (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) β†’ 𝑅 ∈ TosetRel )
13 tsrps 18573 . . . . . . . . . . 11 (𝑅 ∈ TosetRel β†’ 𝑅 ∈ PosetRel)
1412, 13syl 17 . . . . . . . . . 10 (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) β†’ 𝑅 ∈ PosetRel)
15 simprl 769 . . . . . . . . . 10 (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) β†’ 𝐴𝑅𝐡)
16 psasym 18562 . . . . . . . . . . 11 ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐡 ∧ 𝐡𝑅𝐴) β†’ 𝐴 = 𝐡)
17163expia 1118 . . . . . . . . . 10 ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐡) β†’ (𝐡𝑅𝐴 β†’ 𝐴 = 𝐡))
1814, 15, 17syl2anc 582 . . . . . . . . 9 (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) β†’ (𝐡𝑅𝐴 β†’ 𝐴 = 𝐡))
1918necon3ad 2943 . . . . . . . 8 (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) β†’ (𝐴 β‰  𝐡 β†’ Β¬ 𝐡𝑅𝐴))
2011, 19mpd 15 . . . . . . 7 (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) β†’ Β¬ 𝐡𝑅𝐴)
2120adantr 479 . . . . . 6 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…) β†’ Β¬ 𝐡𝑅𝐴)
2210, 6, 21elrabd 3678 . . . . 5 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…) β†’ 𝐴 ∈ {π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯})
23 breq1 5147 . . . . . . 7 (π‘₯ = 𝐡 β†’ (π‘₯𝑅𝐴 ↔ 𝐡𝑅𝐴))
2423notbid 317 . . . . . 6 (π‘₯ = 𝐡 β†’ (Β¬ π‘₯𝑅𝐴 ↔ Β¬ 𝐡𝑅𝐴))
2524, 2, 21elrabd 3678 . . . . 5 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…) β†’ 𝐡 ∈ {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴})
26 simpr 483 . . . . 5 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…) β†’ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…)
27 eleq2 2814 . . . . . . 7 (π‘š = {π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} β†’ (𝐴 ∈ π‘š ↔ 𝐴 ∈ {π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯}))
28 ineq1 4200 . . . . . . . 8 (π‘š = {π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} β†’ (π‘š ∩ 𝑛) = ({π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∩ 𝑛))
2928eqeq1d 2727 . . . . . . 7 (π‘š = {π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} β†’ ((π‘š ∩ 𝑛) = βˆ… ↔ ({π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∩ 𝑛) = βˆ…))
3027, 293anbi13d 1434 . . . . . 6 (π‘š = {π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} β†’ ((𝐴 ∈ π‘š ∧ 𝐡 ∈ 𝑛 ∧ (π‘š ∩ 𝑛) = βˆ…) ↔ (𝐴 ∈ {π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∧ 𝐡 ∈ 𝑛 ∧ ({π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∩ 𝑛) = βˆ…)))
31 eleq2 2814 . . . . . . 7 (𝑛 = {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴} β†’ (𝐡 ∈ 𝑛 ↔ 𝐡 ∈ {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴}))
32 ineq2 4201 . . . . . . . . 9 (𝑛 = {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴} β†’ ({π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∩ 𝑛) = ({π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∩ {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴}))
33 inrab 4302 . . . . . . . . 9 ({π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∩ {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴}) = {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)}
3432, 33eqtrdi 2781 . . . . . . . 8 (𝑛 = {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴} β†’ ({π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∩ 𝑛) = {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)})
3534eqeq1d 2727 . . . . . . 7 (𝑛 = {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴} β†’ (({π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∩ 𝑛) = βˆ… ↔ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…))
3631, 353anbi23d 1435 . . . . . 6 (𝑛 = {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴} β†’ ((𝐴 ∈ {π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∧ 𝐡 ∈ 𝑛 ∧ ({π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∩ 𝑛) = βˆ…) ↔ (𝐴 ∈ {π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∧ 𝐡 ∈ {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴} ∧ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…)))
3730, 36rspc2ev 3616 . . . . 5 (({π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∈ (ordTopβ€˜π‘…) ∧ {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴} ∈ (ordTopβ€˜π‘…) ∧ (𝐴 ∈ {π‘₯ ∈ 𝑋 ∣ Β¬ 𝐡𝑅π‘₯} ∧ 𝐡 ∈ {π‘₯ ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝐴} ∧ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…)) β†’ βˆƒπ‘š ∈ (ordTopβ€˜π‘…)βˆƒπ‘› ∈ (ordTopβ€˜π‘…)(𝐴 ∈ π‘š ∧ 𝐡 ∈ 𝑛 ∧ (π‘š ∩ 𝑛) = βˆ…))
385, 8, 22, 25, 26, 37syl113anc 1379 . . . 4 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ {π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ…) β†’ βˆƒπ‘š ∈ (ordTopβ€˜π‘…)βˆƒπ‘› ∈ (ordTopβ€˜π‘…)(𝐴 ∈ π‘š ∧ 𝐡 ∈ 𝑛 ∧ (π‘š ∩ 𝑛) = βˆ…))
3938ex 411 . . 3 (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) β†’ ({π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} = βˆ… β†’ βˆƒπ‘š ∈ (ordTopβ€˜π‘…)βˆƒπ‘› ∈ (ordTopβ€˜π‘…)(𝐴 ∈ π‘š ∧ 𝐡 ∈ 𝑛 ∧ (π‘š ∩ 𝑛) = βˆ…)))
40 rabn0 4382 . . . 4 ({π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} β‰  βˆ… ↔ βˆƒπ‘₯ ∈ 𝑋 (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))
41 simpll1 1209 . . . . . . 7 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ 𝑅 ∈ TosetRel )
42 simprl 769 . . . . . . 7 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ π‘₯ ∈ 𝑋)
433ordtopn2 23112 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ π‘₯ ∈ 𝑋) β†’ {𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∈ (ordTopβ€˜π‘…))
4441, 42, 43syl2anc 582 . . . . . 6 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ {𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∈ (ordTopβ€˜π‘…))
453ordtopn1 23111 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ π‘₯ ∈ 𝑋) β†’ {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯} ∈ (ordTopβ€˜π‘…))
4641, 42, 45syl2anc 582 . . . . . 6 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯} ∈ (ordTopβ€˜π‘…))
47 breq2 5148 . . . . . . . 8 (𝑦 = 𝐴 β†’ (π‘₯𝑅𝑦 ↔ π‘₯𝑅𝐴))
4847notbid 317 . . . . . . 7 (𝑦 = 𝐴 β†’ (Β¬ π‘₯𝑅𝑦 ↔ Β¬ π‘₯𝑅𝐴))
49 simpll2 1210 . . . . . . 7 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ 𝐴 ∈ 𝑋)
50 simprrr 780 . . . . . . 7 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ Β¬ π‘₯𝑅𝐴)
5148, 49, 50elrabd 3678 . . . . . 6 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ 𝐴 ∈ {𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦})
52 breq1 5147 . . . . . . . 8 (𝑦 = 𝐡 β†’ (𝑦𝑅π‘₯ ↔ 𝐡𝑅π‘₯))
5352notbid 317 . . . . . . 7 (𝑦 = 𝐡 β†’ (Β¬ 𝑦𝑅π‘₯ ↔ Β¬ 𝐡𝑅π‘₯))
54 simpll3 1211 . . . . . . 7 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ 𝐡 ∈ 𝑋)
55 simprrl 779 . . . . . . 7 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ Β¬ 𝐡𝑅π‘₯)
5653, 54, 55elrabd 3678 . . . . . 6 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ 𝐡 ∈ {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯})
5741, 42jca 510 . . . . . . . . . 10 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ (𝑅 ∈ TosetRel ∧ π‘₯ ∈ 𝑋))
583tsrlin 18571 . . . . . . . . . . 11 ((𝑅 ∈ TosetRel ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯𝑅𝑦 ∨ 𝑦𝑅π‘₯))
59583expa 1115 . . . . . . . . . 10 (((𝑅 ∈ TosetRel ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯𝑅𝑦 ∨ 𝑦𝑅π‘₯))
6057, 59sylan 578 . . . . . . . . 9 (((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯𝑅𝑦 ∨ 𝑦𝑅π‘₯))
61 oran 987 . . . . . . . . 9 ((π‘₯𝑅𝑦 ∨ 𝑦𝑅π‘₯) ↔ Β¬ (Β¬ π‘₯𝑅𝑦 ∧ Β¬ 𝑦𝑅π‘₯))
6260, 61sylib 217 . . . . . . . 8 (((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) ∧ 𝑦 ∈ 𝑋) β†’ Β¬ (Β¬ π‘₯𝑅𝑦 ∧ Β¬ 𝑦𝑅π‘₯))
6362ralrimiva 3136 . . . . . . 7 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ βˆ€π‘¦ ∈ 𝑋 Β¬ (Β¬ π‘₯𝑅𝑦 ∧ Β¬ 𝑦𝑅π‘₯))
64 rabeq0 4381 . . . . . . 7 ({𝑦 ∈ 𝑋 ∣ (Β¬ π‘₯𝑅𝑦 ∧ Β¬ 𝑦𝑅π‘₯)} = βˆ… ↔ βˆ€π‘¦ ∈ 𝑋 Β¬ (Β¬ π‘₯𝑅𝑦 ∧ Β¬ 𝑦𝑅π‘₯))
6563, 64sylibr 233 . . . . . 6 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ {𝑦 ∈ 𝑋 ∣ (Β¬ π‘₯𝑅𝑦 ∧ Β¬ 𝑦𝑅π‘₯)} = βˆ…)
66 eleq2 2814 . . . . . . . 8 (π‘š = {𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} β†’ (𝐴 ∈ π‘š ↔ 𝐴 ∈ {𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦}))
67 ineq1 4200 . . . . . . . . 9 (π‘š = {𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} β†’ (π‘š ∩ 𝑛) = ({𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∩ 𝑛))
6867eqeq1d 2727 . . . . . . . 8 (π‘š = {𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} β†’ ((π‘š ∩ 𝑛) = βˆ… ↔ ({𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∩ 𝑛) = βˆ…))
6966, 683anbi13d 1434 . . . . . . 7 (π‘š = {𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} β†’ ((𝐴 ∈ π‘š ∧ 𝐡 ∈ 𝑛 ∧ (π‘š ∩ 𝑛) = βˆ…) ↔ (𝐴 ∈ {𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∧ 𝐡 ∈ 𝑛 ∧ ({𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∩ 𝑛) = βˆ…)))
70 eleq2 2814 . . . . . . . 8 (𝑛 = {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯} β†’ (𝐡 ∈ 𝑛 ↔ 𝐡 ∈ {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯}))
71 ineq2 4201 . . . . . . . . . 10 (𝑛 = {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯} β†’ ({𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∩ 𝑛) = ({𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∩ {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯}))
72 inrab 4302 . . . . . . . . . 10 ({𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∩ {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯}) = {𝑦 ∈ 𝑋 ∣ (Β¬ π‘₯𝑅𝑦 ∧ Β¬ 𝑦𝑅π‘₯)}
7371, 72eqtrdi 2781 . . . . . . . . 9 (𝑛 = {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯} β†’ ({𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∩ 𝑛) = {𝑦 ∈ 𝑋 ∣ (Β¬ π‘₯𝑅𝑦 ∧ Β¬ 𝑦𝑅π‘₯)})
7473eqeq1d 2727 . . . . . . . 8 (𝑛 = {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯} β†’ (({𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∩ 𝑛) = βˆ… ↔ {𝑦 ∈ 𝑋 ∣ (Β¬ π‘₯𝑅𝑦 ∧ Β¬ 𝑦𝑅π‘₯)} = βˆ…))
7570, 743anbi23d 1435 . . . . . . 7 (𝑛 = {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯} β†’ ((𝐴 ∈ {𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∧ 𝐡 ∈ 𝑛 ∧ ({𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∩ 𝑛) = βˆ…) ↔ (𝐴 ∈ {𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∧ 𝐡 ∈ {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯} ∧ {𝑦 ∈ 𝑋 ∣ (Β¬ π‘₯𝑅𝑦 ∧ Β¬ 𝑦𝑅π‘₯)} = βˆ…)))
7669, 75rspc2ev 3616 . . . . . 6 (({𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∈ (ordTopβ€˜π‘…) ∧ {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯} ∈ (ordTopβ€˜π‘…) ∧ (𝐴 ∈ {𝑦 ∈ 𝑋 ∣ Β¬ π‘₯𝑅𝑦} ∧ 𝐡 ∈ {𝑦 ∈ 𝑋 ∣ Β¬ 𝑦𝑅π‘₯} ∧ {𝑦 ∈ 𝑋 ∣ (Β¬ π‘₯𝑅𝑦 ∧ Β¬ 𝑦𝑅π‘₯)} = βˆ…)) β†’ βˆƒπ‘š ∈ (ordTopβ€˜π‘…)βˆƒπ‘› ∈ (ordTopβ€˜π‘…)(𝐴 ∈ π‘š ∧ 𝐡 ∈ 𝑛 ∧ (π‘š ∩ 𝑛) = βˆ…))
7744, 46, 51, 56, 65, 76syl113anc 1379 . . . . 5 ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) ∧ (π‘₯ ∈ 𝑋 ∧ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴))) β†’ βˆƒπ‘š ∈ (ordTopβ€˜π‘…)βˆƒπ‘› ∈ (ordTopβ€˜π‘…)(𝐴 ∈ π‘š ∧ 𝐡 ∈ 𝑛 ∧ (π‘š ∩ 𝑛) = βˆ…))
7877rexlimdvaa 3146 . . . 4 (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) β†’ (βˆƒπ‘₯ ∈ 𝑋 (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴) β†’ βˆƒπ‘š ∈ (ordTopβ€˜π‘…)βˆƒπ‘› ∈ (ordTopβ€˜π‘…)(𝐴 ∈ π‘š ∧ 𝐡 ∈ 𝑛 ∧ (π‘š ∩ 𝑛) = βˆ…)))
7940, 78biimtrid 241 . . 3 (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) β†’ ({π‘₯ ∈ 𝑋 ∣ (Β¬ 𝐡𝑅π‘₯ ∧ Β¬ π‘₯𝑅𝐴)} β‰  βˆ… β†’ βˆƒπ‘š ∈ (ordTopβ€˜π‘…)βˆƒπ‘› ∈ (ordTopβ€˜π‘…)(𝐴 ∈ π‘š ∧ 𝐡 ∈ 𝑛 ∧ (π‘š ∩ 𝑛) = βˆ…)))
8039, 79pm2.61dne 3018 . 2 (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) ∧ (𝐴𝑅𝐡 ∧ 𝐴 β‰  𝐡)) β†’ βˆƒπ‘š ∈ (ordTopβ€˜π‘…)βˆƒπ‘› ∈ (ordTopβ€˜π‘…)(𝐴 ∈ π‘š ∧ 𝐡 ∈ 𝑛 ∧ (π‘š ∩ 𝑛) = βˆ…))
8180exp32 419 1 ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) β†’ (𝐴𝑅𝐡 β†’ (𝐴 β‰  𝐡 β†’ βˆƒπ‘š ∈ (ordTopβ€˜π‘…)βˆƒπ‘› ∈ (ordTopβ€˜π‘…)(𝐴 ∈ π‘š ∧ 𝐡 ∈ 𝑛 ∧ (π‘š ∩ 𝑛) = βˆ…))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 394   ∨ wo 845   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2930  βˆ€wral 3051  βˆƒwrex 3060  {crab 3419   ∩ cin 3940  βˆ…c0 4319   class class class wbr 5144  dom cdm 5673  β€˜cfv 6543  ordTopcordt 17475  PosetRelcps 18550   TosetRel ctsr 18551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-int 4946  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-om 7866  df-1o 8480  df-en 8958  df-fin 8961  df-fi 9429  df-topgen 17419  df-ordt 17477  df-ps 18552  df-tsr 18553  df-bases 22862
This theorem is referenced by:  ordthaus  23301
  Copyright terms: Public domain W3C validator