Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ordtconnlem1 Structured version   Visualization version   GIF version

Theorem ordtconnlem1 31066
Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 31067. See also reconnlem1 23361. (Contributed by Thierry Arnoux, 14-Sep-2018.)
Hypotheses
Ref Expression
ordtconn.x 𝐵 = (Base‘𝐾)
ordtconn.l = ((le‘𝐾) ∩ (𝐵 × 𝐵))
ordtconn.j 𝐽 = (ordTop‘ )
Assertion
Ref Expression
ordtconnlem1 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → ((𝐽t 𝐴) ∈ Conn → ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)))
Distinct variable groups:   𝑥,𝑟,𝑦,𝐴   𝐵,𝑟,𝑥,𝑦   𝐽,𝑟   𝐾,𝑟,𝑥,𝑦   𝑥, ,𝑦
Allowed substitution hints:   𝐽(𝑥,𝑦)   (𝑟)

Proof of Theorem ordtconnlem1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 nfv 1906 . . . . 5 𝑟(𝐾 ∈ Toset ∧ 𝐴𝐵)
2 nfcv 2974 . . . . . . 7 𝑟𝐴
3 nfra2w 3224 . . . . . . 7 𝑟𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
42, 3nfralw 3222 . . . . . 6 𝑟𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
54nfn 1848 . . . . 5 𝑟 ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
61, 5nfan 1891 . . . 4 𝑟((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
7 tospos 30572 . . . . . . . . . 10 (𝐾 ∈ Toset → 𝐾 ∈ Poset)
8 posprs 17547 . . . . . . . . . 10 (𝐾 ∈ Poset → 𝐾 ∈ Proset )
9 ordtconn.j . . . . . . . . . . 11 𝐽 = (ordTop‘ )
10 ordtconn.l . . . . . . . . . . . . . 14 = ((le‘𝐾) ∩ (𝐵 × 𝐵))
11 fvex 6676 . . . . . . . . . . . . . . 15 (le‘𝐾) ∈ V
1211inex1 5212 . . . . . . . . . . . . . 14 ((le‘𝐾) ∩ (𝐵 × 𝐵)) ∈ V
1310, 12eqeltri 2906 . . . . . . . . . . . . 13 ∈ V
14 eqid 2818 . . . . . . . . . . . . . 14 dom = dom
1514ordttopon 21729 . . . . . . . . . . . . 13 ( ∈ V → (ordTop‘ ) ∈ (TopOn‘dom ))
1613, 15ax-mp 5 . . . . . . . . . . . 12 (ordTop‘ ) ∈ (TopOn‘dom )
17 ordtconn.x . . . . . . . . . . . . . 14 𝐵 = (Base‘𝐾)
1817, 10prsdm 31056 . . . . . . . . . . . . 13 (𝐾 ∈ Proset → dom = 𝐵)
1918fveq2d 6667 . . . . . . . . . . . 12 (𝐾 ∈ Proset → (TopOn‘dom ) = (TopOn‘𝐵))
2016, 19eleqtrid 2916 . . . . . . . . . . 11 (𝐾 ∈ Proset → (ordTop‘ ) ∈ (TopOn‘𝐵))
219, 20eqeltrid 2914 . . . . . . . . . 10 (𝐾 ∈ Proset → 𝐽 ∈ (TopOn‘𝐵))
227, 8, 213syl 18 . . . . . . . . 9 (𝐾 ∈ Toset → 𝐽 ∈ (TopOn‘𝐵))
2322ad3antrrr 726 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐽 ∈ (TopOn‘𝐵))
2423adantlr 711 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → 𝐽 ∈ (TopOn‘𝐵))
25 simpllr 772 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴𝐵)
2625adantlr 711 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → 𝐴𝐵)
27 simpll 763 . . . . . . . . . . . 12 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → 𝐾 ∈ Toset)
2827, 7, 83syl 18 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → 𝐾 ∈ Proset )
29 snex 5322 . . . . . . . . . . . . . . . 16 {𝐵} ∈ V
3017fvexi 6677 . . . . . . . . . . . . . . . . . . 19 𝐵 ∈ V
3130mptex 6977 . . . . . . . . . . . . . . . . . 18 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∈ V
3231rnex 7606 . . . . . . . . . . . . . . . . 17 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∈ V
3330mptex 6977 . . . . . . . . . . . . . . . . . 18 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ∈ V
3433rnex 7606 . . . . . . . . . . . . . . . . 17 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ∈ V
3532, 34unex 7458 . . . . . . . . . . . . . . . 16 (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ∈ V
3629, 35unex 7458 . . . . . . . . . . . . . . 15 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ∈ V
37 ssfii 8871 . . . . . . . . . . . . . . 15 (({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ∈ V → ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))))
3836, 37ax-mp 5 . . . . . . . . . . . . . 14 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))
39 fvex 6676 . . . . . . . . . . . . . . 15 (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))) ∈ V
40 bastg 21502 . . . . . . . . . . . . . . 15 ((fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))) ∈ V → (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))))
4139, 40ax-mp 5 . . . . . . . . . . . . . 14 (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))))
4238, 41sstri 3973 . . . . . . . . . . . . 13 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))))
43 eqid 2818 . . . . . . . . . . . . . . 15 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) = ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
44 eqid 2818 . . . . . . . . . . . . . . 15 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) = ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
4517, 10, 43, 44ordtprsval 31060 . . . . . . . . . . . . . 14 (𝐾 ∈ Proset → (ordTop‘ ) = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))))
469, 45syl5eq 2865 . . . . . . . . . . . . 13 (𝐾 ∈ Proset → 𝐽 = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))))
4742, 46sseqtrrid 4017 . . . . . . . . . . . 12 (𝐾 ∈ Proset → ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ 𝐽)
4847unssbd 4161 . . . . . . . . . . 11 (𝐾 ∈ Proset → (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ⊆ 𝐽)
4928, 48syl 17 . . . . . . . . . 10 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ⊆ 𝐽)
5049unssbd 4161 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ⊆ 𝐽)
51 breq2 5061 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑟 𝑧𝑟 𝑦))
5251notbid 319 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (¬ 𝑟 𝑧 ↔ ¬ 𝑟 𝑦))
5352cbvrabv 3489 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦}
54 breq1 5060 . . . . . . . . . . . . . . 15 (𝑥 = 𝑟 → (𝑥 𝑦𝑟 𝑦))
5554notbid 319 . . . . . . . . . . . . . 14 (𝑥 = 𝑟 → (¬ 𝑥 𝑦 ↔ ¬ 𝑟 𝑦))
5655rabbidv 3478 . . . . . . . . . . . . 13 (𝑥 = 𝑟 → {𝑦𝐵 ∣ ¬ 𝑥 𝑦} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦})
5756rspceeqv 3635 . . . . . . . . . . . 12 ((𝑟𝐵 ∧ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦}) → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
5853, 57mpan2 687 . . . . . . . . . . 11 (𝑟𝐵 → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
5930rabex 5226 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ V
60 eqid 2818 . . . . . . . . . . . . 13 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) = (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
6160elrnmpt 5821 . . . . . . . . . . . 12 ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ V → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6259, 61ax-mp 5 . . . . . . . . . . 11 ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
6358, 62sylibr 235 . . . . . . . . . 10 (𝑟𝐵 → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6463adantl 482 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6550, 64sseldd 3965 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ 𝐽)
6665ad2antrr 722 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ 𝐽)
6749unssad 4160 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ⊆ 𝐽)
68 breq1 5060 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑧 𝑟𝑦 𝑟))
6968notbid 319 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (¬ 𝑧 𝑟 ↔ ¬ 𝑦 𝑟))
7069cbvrabv 3489 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟}
71 breq2 5061 . . . . . . . . . . . . . . 15 (𝑥 = 𝑟 → (𝑦 𝑥𝑦 𝑟))
7271notbid 319 . . . . . . . . . . . . . 14 (𝑥 = 𝑟 → (¬ 𝑦 𝑥 ↔ ¬ 𝑦 𝑟))
7372rabbidv 3478 . . . . . . . . . . . . 13 (𝑥 = 𝑟 → {𝑦𝐵 ∣ ¬ 𝑦 𝑥} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟})
7473rspceeqv 3635 . . . . . . . . . . . 12 ((𝑟𝐵 ∧ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟}) → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7570, 74mpan2 687 . . . . . . . . . . 11 (𝑟𝐵 → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7630rabex 5226 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ V
77 eqid 2818 . . . . . . . . . . . . 13 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) = (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7877elrnmpt 5821 . . . . . . . . . . . 12 ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ V → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
7976, 78ax-mp 5 . . . . . . . . . . 11 ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
8075, 79sylibr 235 . . . . . . . . . 10 (𝑟𝐵 → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
8180adantl 482 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
8267, 81sseldd 3965 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ 𝐽)
8382ad2antrr 722 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ 𝐽)
84 simpll 763 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵))
85 simpr 485 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ¬ 𝑟𝐴)
8684, 85jca 512 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴))
87 simplrl 773 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ∃𝑥𝐴 ¬ 𝑟 𝑥)
88 ssel 3958 . . . . . . . . . . . . . . 15 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
8988ancrd 552 . . . . . . . . . . . . . 14 (𝐴𝐵 → (𝑥𝐴 → (𝑥𝐵𝑥𝐴)))
9089anim1d 610 . . . . . . . . . . . . 13 (𝐴𝐵 → ((𝑥𝐴 ∧ ¬ 𝑟 𝑥) → ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥)))
9190impl 456 . . . . . . . . . . . 12 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
92 elin 4166 . . . . . . . . . . . . 13 (𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ↔ (𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑥𝐴))
93 breq2 5061 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑥 → (𝑟 𝑧𝑟 𝑥))
9493notbid 319 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → (¬ 𝑟 𝑧 ↔ ¬ 𝑟 𝑥))
9594elrab 3677 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ↔ (𝑥𝐵 ∧ ¬ 𝑟 𝑥))
9695anbi1i 623 . . . . . . . . . . . . 13 ((𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑥𝐴) ↔ ((𝑥𝐵 ∧ ¬ 𝑟 𝑥) ∧ 𝑥𝐴))
97 an32 642 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ¬ 𝑟 𝑥) ∧ 𝑥𝐴) ↔ ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
9892, 96, 973bitri 298 . . . . . . . . . . . 12 (𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ↔ ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
9991, 98sylibr 235 . . . . . . . . . . 11 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → 𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴))
10099ne0d 4298 . . . . . . . . . 10 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
10125, 100sylanl1 676 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
102101r19.29an 3285 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ ∃𝑥𝐴 ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
10386, 87, 102syl2anc 584 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
104 simplrr 774 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ∃𝑦𝐴 ¬ 𝑦 𝑟)
105 ssel 3958 . . . . . . . . . . . . . . 15 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
106105ancrd 552 . . . . . . . . . . . . . 14 (𝐴𝐵 → (𝑦𝐴 → (𝑦𝐵𝑦𝐴)))
107106anim1d 610 . . . . . . . . . . . . 13 (𝐴𝐵 → ((𝑦𝐴 ∧ ¬ 𝑦 𝑟) → ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟)))
108107impl 456 . . . . . . . . . . . 12 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
109 elin 4166 . . . . . . . . . . . . 13 (𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ↔ (𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∧ 𝑦𝐴))
11069elrab 3677 . . . . . . . . . . . . . 14 (𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ↔ (𝑦𝐵 ∧ ¬ 𝑦 𝑟))
111110anbi1i 623 . . . . . . . . . . . . 13 ((𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∧ 𝑦𝐴) ↔ ((𝑦𝐵 ∧ ¬ 𝑦 𝑟) ∧ 𝑦𝐴))
112 an32 642 . . . . . . . . . . . . 13 (((𝑦𝐵 ∧ ¬ 𝑦 𝑟) ∧ 𝑦𝐴) ↔ ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
113109, 111, 1123bitri 298 . . . . . . . . . . . 12 (𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ↔ ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
114108, 113sylibr 235 . . . . . . . . . . 11 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → 𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴))
115114ne0d 4298 . . . . . . . . . 10 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
11625, 115sylanl1 676 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
117116r19.29an 3285 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
11886, 104, 117syl2anc 584 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
11917, 10trleile 30580 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑧𝐵) → (𝑟 𝑧𝑧 𝑟))
120 oran 983 . . . . . . . . . . . . . . . 16 ((𝑟 𝑧𝑧 𝑟) ↔ ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
121119, 120sylib 219 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑧𝐵) → ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
1221213expa 1110 . . . . . . . . . . . . . 14 (((𝐾 ∈ Toset ∧ 𝑟𝐵) ∧ 𝑧𝐵) → ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
123122nrexdv 3267 . . . . . . . . . . . . 13 ((𝐾 ∈ Toset ∧ 𝑟𝐵) → ¬ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
124 rabid 3376 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ↔ (𝑧𝐵 ∧ ¬ 𝑟 𝑧))
125 rabid 3376 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ↔ (𝑧𝐵 ∧ ¬ 𝑧 𝑟))
126124, 125anbi12i 626 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∧ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
127 elin 4166 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
128 anandi 672 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∧ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
129126, 127, 1283bitr4i 304 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
130129exbii 1839 . . . . . . . . . . . . . . 15 (∃𝑧 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ∃𝑧(𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
131 nfrab1 3382 . . . . . . . . . . . . . . . . 17 𝑧{𝑧𝐵 ∣ ¬ 𝑟 𝑧}
132 nfrab1 3382 . . . . . . . . . . . . . . . . 17 𝑧{𝑧𝐵 ∣ ¬ 𝑧 𝑟}
133131, 132nfin 4190 . . . . . . . . . . . . . . . 16 𝑧({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟})
134133n0f 4304 . . . . . . . . . . . . . . 15 (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
135 df-rex 3141 . . . . . . . . . . . . . . 15 (∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟) ↔ ∃𝑧(𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
136130, 134, 1353bitr4i 304 . . . . . . . . . . . . . 14 (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ≠ ∅ ↔ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
137136necon1bbii 3062 . . . . . . . . . . . . 13 (¬ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟) ↔ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
138123, 137sylib 219 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
139138adantlr 711 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
140139adantr 481 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
141140ineq1d 4185 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = (∅ ∩ 𝐴))
142 0in 4344 . . . . . . . . 9 (∅ ∩ 𝐴) = ∅
143141, 142syl6eq 2869 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = ∅)
144143adantlr 711 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = ∅)
145 simplr 765 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝑟𝐵)
146 simpr 485 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ¬ 𝑟𝐴)
147 vex 3495 . . . . . . . . . . . . . . 15 𝑟 ∈ V
148147snss 4710 . . . . . . . . . . . . . 14 (𝑟𝐵 ↔ {𝑟} ⊆ 𝐵)
149 eldif 3943 . . . . . . . . . . . . . . . 16 (𝑟 ∈ (𝐵𝐴) ↔ (𝑟𝐵 ∧ ¬ 𝑟𝐴))
150147snss 4710 . . . . . . . . . . . . . . . 16 (𝑟 ∈ (𝐵𝐴) ↔ {𝑟} ⊆ (𝐵𝐴))
151149, 150bitr3i 278 . . . . . . . . . . . . . . 15 ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ {𝑟} ⊆ (𝐵𝐴))
152 ssconb 4111 . . . . . . . . . . . . . . 15 (({𝑟} ⊆ 𝐵𝐴𝐵) → ({𝑟} ⊆ (𝐵𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
153151, 152syl5bb 284 . . . . . . . . . . . . . 14 (({𝑟} ⊆ 𝐵𝐴𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
154148, 153sylanb 581 . . . . . . . . . . . . 13 ((𝑟𝐵𝐴𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
155154adantl 482 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ (𝑟𝐵𝐴𝐵)) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
156155anass1rs 651 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
157156adantr 481 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
158145, 146, 157mpbi2and 708 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ (𝐵 ∖ {𝑟}))
1597ad3antrrr 726 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐾 ∈ Poset)
160 nfv 1906 . . . . . . . . . . 11 𝑧(𝐾 ∈ Poset ∧ 𝑟𝐵)
161131, 132nfun 4138 . . . . . . . . . . 11 𝑧({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟})
162 nfcv 2974 . . . . . . . . . . 11 𝑧(𝐵 ∖ {𝑟})
163 ianor 975 . . . . . . . . . . . . . . 15 (¬ (𝑟 𝑧𝑧 𝑟) ↔ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟))
16417, 10posrasymb 30571 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((𝑟 𝑧𝑧 𝑟) ↔ 𝑟 = 𝑧))
165 equcom 2016 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑧𝑧 = 𝑟)
166164, 165syl6bb 288 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((𝑟 𝑧𝑧 𝑟) ↔ 𝑧 = 𝑟))
167166necon3bbid 3050 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → (¬ (𝑟 𝑧𝑧 𝑟) ↔ 𝑧𝑟))
168163, 167syl5bbr 286 . . . . . . . . . . . . . 14 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟) ↔ 𝑧𝑟))
1691683expia 1113 . . . . . . . . . . . . 13 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → (𝑧𝐵 → ((¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟) ↔ 𝑧𝑟)))
170169pm5.32d 577 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ (𝑧𝐵𝑧𝑟)))
171124, 125orbi12i 908 . . . . . . . . . . . . 13 ((𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∨ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∨ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
172 elun 4122 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∨ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
173 andi 1001 . . . . . . . . . . . . 13 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∨ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
174171, 172, 1733bitr4ri 305 . . . . . . . . . . . 12 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
175 eldifsn 4711 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐵 ∖ {𝑟}) ↔ (𝑧𝐵𝑧𝑟))
176175bicomi 225 . . . . . . . . . . . 12 ((𝑧𝐵𝑧𝑟) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟}))
177170, 174, 1763bitr3g 314 . . . . . . . . . . 11 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟})))
178160, 161, 162, 177eqrd 3983 . . . . . . . . . 10 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = (𝐵 ∖ {𝑟}))
179159, 145, 178syl2anc 584 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = (𝐵 ∖ {𝑟}))
180158, 179sseqtrrd 4005 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
181180adantlr 711 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
18224, 26, 66, 83, 103, 118, 144, 181nconnsubb 21959 . . . . . 6 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ¬ (𝐽t 𝐴) ∈ Conn)
183182anasss 467 . . . . 5 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Conn)
184183adantllr 715 . . . 4 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) ∧ 𝑟𝐵) ∧ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Conn)
185 rexanali 3262 . . . . . . . . . . 11 (∃𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
186185rexbii 3244 . . . . . . . . . 10 (∃𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑦𝐴 ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
187 rexcom 3352 . . . . . . . . . 10 (∃𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
188 rexnal 3235 . . . . . . . . . 10 (∃𝑦𝐴 ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
189186, 187, 1883bitr3i 302 . . . . . . . . 9 (∃𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
190189rexbii 3244 . . . . . . . 8 (∃𝑥𝐴𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑥𝐴 ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
191 rexcom 3352 . . . . . . . 8 (∃𝑥𝐴𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
192 rexnal 3235 . . . . . . . 8 (∃𝑥𝐴 ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
193190, 191, 1923bitr3i 302 . . . . . . 7 (∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
194 r19.41v 3344 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
195194rexbii 3244 . . . . . . . . 9 (∃𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑥𝐴 (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
196 r19.41v 3344 . . . . . . . . 9 (∃𝑥𝐴 (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ (∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
197 reeanv 3365 . . . . . . . . . 10 (∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ↔ (∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦))
198197anbi1i 623 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
199195, 196, 1983bitri 298 . . . . . . . 8 (∃𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
200199rexbii 3244 . . . . . . 7 (∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
201193, 200bitr3i 278 . . . . . 6 (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
20227ad2antrr 722 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝐾 ∈ Toset)
20325sselda 3964 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝐵)
204 simpllr 772 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑟𝐵)
20517, 10trleile 30580 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ 𝑥𝐵𝑟𝐵) → (𝑥 𝑟𝑟 𝑥))
206202, 203, 204, 205syl3anc 1363 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (𝑥 𝑟𝑟 𝑥))
207 simpr 485 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝐴)
208 simplr 765 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ¬ 𝑟𝐴)
209 nelne2 3112 . . . . . . . . . . . . . . 15 ((𝑥𝐴 ∧ ¬ 𝑟𝐴) → 𝑥𝑟)
210207, 208, 209syl2anc 584 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝑟)
211159adantr 481 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝐾 ∈ Poset)
21217, 10posrasymb 30571 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑥𝐵𝑟𝐵) → ((𝑥 𝑟𝑟 𝑥) ↔ 𝑥 = 𝑟))
213212necon3bbid 3050 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑥𝐵𝑟𝐵) → (¬ (𝑥 𝑟𝑟 𝑥) ↔ 𝑥𝑟))
214211, 203, 204, 213syl3anc 1363 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (¬ (𝑥 𝑟𝑟 𝑥) ↔ 𝑥𝑟))
215210, 214mpbird 258 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ¬ (𝑥 𝑟𝑟 𝑥))
216206, 215jca 512 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ((𝑥 𝑟𝑟 𝑥) ∧ ¬ (𝑥 𝑟𝑟 𝑥)))
217 pm5.17 1005 . . . . . . . . . . . 12 (((𝑥 𝑟𝑟 𝑥) ∧ ¬ (𝑥 𝑟𝑟 𝑥)) ↔ (𝑥 𝑟 ↔ ¬ 𝑟 𝑥))
218216, 217sylib 219 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (𝑥 𝑟 ↔ ¬ 𝑟 𝑥))
219218rexbidva 3293 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (∃𝑥𝐴 𝑥 𝑟 ↔ ∃𝑥𝐴 ¬ 𝑟 𝑥))
22027ad2antrr 722 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝐾 ∈ Toset)
221 simpllr 772 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑟𝐵)
22225sselda 3964 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝐵)
22317, 10trleile 30580 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑦𝐵) → (𝑟 𝑦𝑦 𝑟))
224220, 221, 222, 223syl3anc 1363 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (𝑟 𝑦𝑦 𝑟))
225 simpr 485 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝐴)
226 simplr 765 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ¬ 𝑟𝐴)
227 nelne2 3112 . . . . . . . . . . . . . . . 16 ((𝑦𝐴 ∧ ¬ 𝑟𝐴) → 𝑦𝑟)
228225, 226, 227syl2anc 584 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝑟)
229228necomd 3068 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑟𝑦)
230159adantr 481 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝐾 ∈ Poset)
23117, 10posrasymb 30571 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑦𝐵) → ((𝑟 𝑦𝑦 𝑟) ↔ 𝑟 = 𝑦))
232231necon3bbid 3050 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑦𝐵) → (¬ (𝑟 𝑦𝑦 𝑟) ↔ 𝑟𝑦))
233230, 221, 222, 232syl3anc 1363 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (¬ (𝑟 𝑦𝑦 𝑟) ↔ 𝑟𝑦))
234229, 233mpbird 258 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ¬ (𝑟 𝑦𝑦 𝑟))
235224, 234jca 512 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ((𝑟 𝑦𝑦 𝑟) ∧ ¬ (𝑟 𝑦𝑦 𝑟)))
236 pm5.17 1005 . . . . . . . . . . . 12 (((𝑟 𝑦𝑦 𝑟) ∧ ¬ (𝑟 𝑦𝑦 𝑟)) ↔ (𝑟 𝑦 ↔ ¬ 𝑦 𝑟))
237235, 236sylib 219 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (𝑟 𝑦 ↔ ¬ 𝑦 𝑟))
238237rexbidva 3293 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (∃𝑦𝐴 𝑟 𝑦 ↔ ∃𝑦𝐴 ¬ 𝑦 𝑟))
239219, 238anbi12d 630 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ↔ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)))
240239ex 413 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (¬ 𝑟𝐴 → ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ↔ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟))))
241240pm5.32rd 578 . . . . . . 7 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
242241rexbidva 3293 . . . . . 6 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
243201, 242syl5bb 284 . . . . 5 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
244243biimpa 477 . . . 4 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) → ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴))
2456, 184, 244r19.29af 3328 . . 3 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Conn)
246245ex 413 . 2 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) → ¬ (𝐽t 𝐴) ∈ Conn))
247246con4d 115 1 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → ((𝐽t 𝐴) ∈ Conn → ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wex 1771  wcel 2105  wne 3013  wral 3135  wrex 3136  {crab 3139  Vcvv 3492  cdif 3930  cun 3931  cin 3932  wss 3933  c0 4288  {csn 4557   class class class wbr 5057  cmpt 5137   × cxp 5546  dom cdm 5548  ran crn 5549  cfv 6348  (class class class)co 7145  ficfi 8862  Basecbs 16471  lecple 16560  t crest 16682  topGenctg 16699  ordTopcordt 16760   Proset cproset 17524  Posetcpo 17538  Tosetctos 17631  TopOnctopon 21446  Conncconn 21947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-er 8278  df-en 8498  df-fin 8501  df-fi 8863  df-rest 16684  df-topgen 16705  df-ordt 16762  df-proset 17526  df-poset 17544  df-toset 17632  df-top 21430  df-topon 21447  df-bases 21482  df-cld 21555  df-conn 21948
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator