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 30568
Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 30569. See also reconnlem1 23037. (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 1957 . . . . 5 𝑟(𝐾 ∈ Toset ∧ 𝐴𝐵)
2 nfcv 2933 . . . . . . 7 𝑟𝐴
3 nfra2 3127 . . . . . . 7 𝑟𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
42, 3nfral 3126 . . . . . 6 𝑟𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
54nfn 1902 . . . . 5 𝑟 ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
61, 5nfan 1946 . . . 4 𝑟((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
7 tospos 30220 . . . . . . . . . 10 (𝐾 ∈ Toset → 𝐾 ∈ Poset)
8 posprs 17335 . . . . . . . . . 10 (𝐾 ∈ Poset → 𝐾 ∈ Proset )
9 ordtconn.j . . . . . . . . . . 11 𝐽 = (ordTop‘ )
10 ordtconn.l . . . . . . . . . . . . . 14 = ((le‘𝐾) ∩ (𝐵 × 𝐵))
11 fvex 6459 . . . . . . . . . . . . . . 15 (le‘𝐾) ∈ V
1211inex1 5036 . . . . . . . . . . . . . 14 ((le‘𝐾) ∩ (𝐵 × 𝐵)) ∈ V
1310, 12eqeltri 2854 . . . . . . . . . . . . 13 ∈ V
14 eqid 2777 . . . . . . . . . . . . . 14 dom = dom
1514ordttopon 21405 . . . . . . . . . . . . 13 ( ∈ V → (ordTop‘ ) ∈ (TopOn‘dom ))
1613, 15ax-mp 5 . . . . . . . . . . . 12 (ordTop‘ ) ∈ (TopOn‘dom )
17 ordtconn.x . . . . . . . . . . . . . 14 𝐵 = (Base‘𝐾)
1817, 10prsdm 30558 . . . . . . . . . . . . 13 (𝐾 ∈ Proset → dom = 𝐵)
1918fveq2d 6450 . . . . . . . . . . . 12 (𝐾 ∈ Proset → (TopOn‘dom ) = (TopOn‘𝐵))
2016, 19syl5eleq 2864 . . . . . . . . . . 11 (𝐾 ∈ Proset → (ordTop‘ ) ∈ (TopOn‘𝐵))
219, 20syl5eqel 2862 . . . . . . . . . 10 (𝐾 ∈ Proset → 𝐽 ∈ (TopOn‘𝐵))
227, 8, 213syl 18 . . . . . . . . 9 (𝐾 ∈ Toset → 𝐽 ∈ (TopOn‘𝐵))
2322ad3antrrr 720 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐽 ∈ (TopOn‘𝐵))
2423adantlr 705 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → 𝐽 ∈ (TopOn‘𝐵))
25 simpllr 766 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴𝐵)
2625adantlr 705 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → 𝐴𝐵)
27 simpll 757 . . . . . . . . . . . 12 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → 𝐾 ∈ Toset)
2827, 7, 83syl 18 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → 𝐾 ∈ Proset )
29 snex 5140 . . . . . . . . . . . . . . . 16 {𝐵} ∈ V
3017fvexi 6460 . . . . . . . . . . . . . . . . . . 19 𝐵 ∈ V
3130mptex 6758 . . . . . . . . . . . . . . . . . 18 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∈ V
3231rnex 7379 . . . . . . . . . . . . . . . . 17 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∈ V
3330mptex 6758 . . . . . . . . . . . . . . . . . 18 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ∈ V
3433rnex 7379 . . . . . . . . . . . . . . . . 17 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ∈ V
3532, 34unex 7233 . . . . . . . . . . . . . . . 16 (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ∈ V
3629, 35unex 7233 . . . . . . . . . . . . . . 15 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ∈ V
37 ssfii 8613 . . . . . . . . . . . . . . 15 (({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ∈ V → ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))))
3836, 37ax-mp 5 . . . . . . . . . . . . . 14 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))
39 fvex 6459 . . . . . . . . . . . . . . 15 (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))) ∈ V
40 bastg 21178 . . . . . . . . . . . . . . 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 3829 . . . . . . . . . . . . 13 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))))
43 eqid 2777 . . . . . . . . . . . . . . 15 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) = ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
44 eqid 2777 . . . . . . . . . . . . . . 15 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) = ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
4517, 10, 43, 44ordtprsval 30562 . . . . . . . . . . . . . 14 (𝐾 ∈ Proset → (ordTop‘ ) = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))))
469, 45syl5eq 2825 . . . . . . . . . . . . 13 (𝐾 ∈ Proset → 𝐽 = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))))
4742, 46syl5sseqr 3872 . . . . . . . . . . . 12 (𝐾 ∈ Proset → ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ 𝐽)
4847unssbd 4013 . . . . . . . . . . 11 (𝐾 ∈ Proset → (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ⊆ 𝐽)
4928, 48syl 17 . . . . . . . . . 10 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ⊆ 𝐽)
5049unssbd 4013 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ⊆ 𝐽)
51 breq2 4890 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑟 𝑧𝑟 𝑦))
5251notbid 310 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (¬ 𝑟 𝑧 ↔ ¬ 𝑟 𝑦))
5352cbvrabv 3395 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦}
54 breq1 4889 . . . . . . . . . . . . . . 15 (𝑥 = 𝑟 → (𝑥 𝑦𝑟 𝑦))
5554notbid 310 . . . . . . . . . . . . . 14 (𝑥 = 𝑟 → (¬ 𝑥 𝑦 ↔ ¬ 𝑟 𝑦))
5655rabbidv 3385 . . . . . . . . . . . . 13 (𝑥 = 𝑟 → {𝑦𝐵 ∣ ¬ 𝑥 𝑦} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦})
5756rspceeqv 3528 . . . . . . . . . . . 12 ((𝑟𝐵 ∧ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦}) → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
5853, 57mpan2 681 . . . . . . . . . . 11 (𝑟𝐵 → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
5930rabex 5049 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ V
60 eqid 2777 . . . . . . . . . . . . 13 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) = (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
6160elrnmpt 5618 . . . . . . . . . . . 12 ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ V → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6259, 61ax-mp 5 . . . . . . . . . . 11 ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
6358, 62sylibr 226 . . . . . . . . . 10 (𝑟𝐵 → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6463adantl 475 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6550, 64sseldd 3821 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ 𝐽)
6665ad2antrr 716 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ 𝐽)
6749unssad 4012 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ⊆ 𝐽)
68 breq1 4889 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑧 𝑟𝑦 𝑟))
6968notbid 310 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (¬ 𝑧 𝑟 ↔ ¬ 𝑦 𝑟))
7069cbvrabv 3395 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟}
71 breq2 4890 . . . . . . . . . . . . . . 15 (𝑥 = 𝑟 → (𝑦 𝑥𝑦 𝑟))
7271notbid 310 . . . . . . . . . . . . . 14 (𝑥 = 𝑟 → (¬ 𝑦 𝑥 ↔ ¬ 𝑦 𝑟))
7372rabbidv 3385 . . . . . . . . . . . . 13 (𝑥 = 𝑟 → {𝑦𝐵 ∣ ¬ 𝑦 𝑥} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟})
7473rspceeqv 3528 . . . . . . . . . . . 12 ((𝑟𝐵 ∧ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟}) → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7570, 74mpan2 681 . . . . . . . . . . 11 (𝑟𝐵 → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7630rabex 5049 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ V
77 eqid 2777 . . . . . . . . . . . . 13 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) = (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7877elrnmpt 5618 . . . . . . . . . . . 12 ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ V → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
7976, 78ax-mp 5 . . . . . . . . . . 11 ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
8075, 79sylibr 226 . . . . . . . . . 10 (𝑟𝐵 → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
8180adantl 475 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
8267, 81sseldd 3821 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ 𝐽)
8382ad2antrr 716 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ 𝐽)
84 simpll 757 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵))
85 simpr 479 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ¬ 𝑟𝐴)
8684, 85jca 507 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴))
87 simplrl 767 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ∃𝑥𝐴 ¬ 𝑟 𝑥)
88 ssel 3814 . . . . . . . . . . . . . . 15 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
8988ancrd 547 . . . . . . . . . . . . . 14 (𝐴𝐵 → (𝑥𝐴 → (𝑥𝐵𝑥𝐴)))
9089anim1d 604 . . . . . . . . . . . . 13 (𝐴𝐵 → ((𝑥𝐴 ∧ ¬ 𝑟 𝑥) → ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥)))
9190impl 449 . . . . . . . . . . . 12 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
92 elin 4018 . . . . . . . . . . . . 13 (𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ↔ (𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑥𝐴))
93 breq2 4890 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑥 → (𝑟 𝑧𝑟 𝑥))
9493notbid 310 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → (¬ 𝑟 𝑧 ↔ ¬ 𝑟 𝑥))
9594elrab 3571 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ↔ (𝑥𝐵 ∧ ¬ 𝑟 𝑥))
9695anbi1i 617 . . . . . . . . . . . . 13 ((𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑥𝐴) ↔ ((𝑥𝐵 ∧ ¬ 𝑟 𝑥) ∧ 𝑥𝐴))
97 an32 636 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ¬ 𝑟 𝑥) ∧ 𝑥𝐴) ↔ ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
9892, 96, 973bitri 289 . . . . . . . . . . . 12 (𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ↔ ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
9991, 98sylibr 226 . . . . . . . . . . 11 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → 𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴))
10099ne0d 4149 . . . . . . . . . 10 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
10125, 100sylanl1 670 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
102101r19.29an 3262 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ ∃𝑥𝐴 ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
10386, 87, 102syl2anc 579 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
104 simplrr 768 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ∃𝑦𝐴 ¬ 𝑦 𝑟)
105 ssel 3814 . . . . . . . . . . . . . . 15 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
106105ancrd 547 . . . . . . . . . . . . . 14 (𝐴𝐵 → (𝑦𝐴 → (𝑦𝐵𝑦𝐴)))
107106anim1d 604 . . . . . . . . . . . . 13 (𝐴𝐵 → ((𝑦𝐴 ∧ ¬ 𝑦 𝑟) → ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟)))
108107impl 449 . . . . . . . . . . . 12 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
109 elin 4018 . . . . . . . . . . . . 13 (𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ↔ (𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∧ 𝑦𝐴))
11069elrab 3571 . . . . . . . . . . . . . 14 (𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ↔ (𝑦𝐵 ∧ ¬ 𝑦 𝑟))
111110anbi1i 617 . . . . . . . . . . . . 13 ((𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∧ 𝑦𝐴) ↔ ((𝑦𝐵 ∧ ¬ 𝑦 𝑟) ∧ 𝑦𝐴))
112 an32 636 . . . . . . . . . . . . 13 (((𝑦𝐵 ∧ ¬ 𝑦 𝑟) ∧ 𝑦𝐴) ↔ ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
113109, 111, 1123bitri 289 . . . . . . . . . . . 12 (𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ↔ ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
114108, 113sylibr 226 . . . . . . . . . . 11 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → 𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴))
115114ne0d 4149 . . . . . . . . . 10 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
11625, 115sylanl1 670 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
117116r19.29an 3262 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
11886, 104, 117syl2anc 579 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
11917, 10trleile 30228 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑧𝐵) → (𝑟 𝑧𝑧 𝑟))
120 oran 975 . . . . . . . . . . . . . . . 16 ((𝑟 𝑧𝑧 𝑟) ↔ ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
121119, 120sylib 210 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑧𝐵) → ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
1221213expa 1108 . . . . . . . . . . . . . 14 (((𝐾 ∈ Toset ∧ 𝑟𝐵) ∧ 𝑧𝐵) → ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
123122nrexdv 3181 . . . . . . . . . . . . 13 ((𝐾 ∈ Toset ∧ 𝑟𝐵) → ¬ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
124 rabid 3301 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ↔ (𝑧𝐵 ∧ ¬ 𝑟 𝑧))
125 rabid 3301 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ↔ (𝑧𝐵 ∧ ¬ 𝑧 𝑟))
126124, 125anbi12i 620 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∧ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
127 elin 4018 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
128 anandi 666 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∧ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
129126, 127, 1283bitr4i 295 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
130129exbii 1892 . . . . . . . . . . . . . . 15 (∃𝑧 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ∃𝑧(𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
131 nfrab1 3308 . . . . . . . . . . . . . . . . 17 𝑧{𝑧𝐵 ∣ ¬ 𝑟 𝑧}
132 nfrab1 3308 . . . . . . . . . . . . . . . . 17 𝑧{𝑧𝐵 ∣ ¬ 𝑧 𝑟}
133131, 132nfin 4040 . . . . . . . . . . . . . . . 16 𝑧({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟})
134133n0f 4155 . . . . . . . . . . . . . . 15 (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
135 df-rex 3095 . . . . . . . . . . . . . . 15 (∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟) ↔ ∃𝑧(𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
136130, 134, 1353bitr4i 295 . . . . . . . . . . . . . 14 (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ≠ ∅ ↔ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
137136necon1bbii 3017 . . . . . . . . . . . . 13 (¬ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟) ↔ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
138123, 137sylib 210 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
139138adantlr 705 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
140139adantr 474 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
141140ineq1d 4035 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = (∅ ∩ 𝐴))
142 0in 4194 . . . . . . . . 9 (∅ ∩ 𝐴) = ∅
143141, 142syl6eq 2829 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = ∅)
144143adantlr 705 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = ∅)
145 simplr 759 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝑟𝐵)
146 simpr 479 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ¬ 𝑟𝐴)
147 vex 3400 . . . . . . . . . . . . . . 15 𝑟 ∈ V
148147snss 4548 . . . . . . . . . . . . . 14 (𝑟𝐵 ↔ {𝑟} ⊆ 𝐵)
149 eldif 3801 . . . . . . . . . . . . . . . 16 (𝑟 ∈ (𝐵𝐴) ↔ (𝑟𝐵 ∧ ¬ 𝑟𝐴))
150147snss 4548 . . . . . . . . . . . . . . . 16 (𝑟 ∈ (𝐵𝐴) ↔ {𝑟} ⊆ (𝐵𝐴))
151149, 150bitr3i 269 . . . . . . . . . . . . . . 15 ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ {𝑟} ⊆ (𝐵𝐴))
152 ssconb 3965 . . . . . . . . . . . . . . 15 (({𝑟} ⊆ 𝐵𝐴𝐵) → ({𝑟} ⊆ (𝐵𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
153151, 152syl5bb 275 . . . . . . . . . . . . . 14 (({𝑟} ⊆ 𝐵𝐴𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
154148, 153sylanb 576 . . . . . . . . . . . . 13 ((𝑟𝐵𝐴𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
155154adantl 475 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ (𝑟𝐵𝐴𝐵)) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
156155anass1rs 645 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
157156adantr 474 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
158145, 146, 157mpbi2and 702 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ (𝐵 ∖ {𝑟}))
1597ad3antrrr 720 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐾 ∈ Poset)
160 nfv 1957 . . . . . . . . . . 11 𝑧(𝐾 ∈ Poset ∧ 𝑟𝐵)
161131, 132nfun 3991 . . . . . . . . . . 11 𝑧({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟})
162 nfcv 2933 . . . . . . . . . . 11 𝑧(𝐵 ∖ {𝑟})
163 ianor 967 . . . . . . . . . . . . . . 15 (¬ (𝑟 𝑧𝑧 𝑟) ↔ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟))
16417, 10posrasymb 30219 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((𝑟 𝑧𝑧 𝑟) ↔ 𝑟 = 𝑧))
165 equcom 2064 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑧𝑧 = 𝑟)
166164, 165syl6bb 279 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((𝑟 𝑧𝑧 𝑟) ↔ 𝑧 = 𝑟))
167166necon3bbid 3005 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → (¬ (𝑟 𝑧𝑧 𝑟) ↔ 𝑧𝑟))
168163, 167syl5bbr 277 . . . . . . . . . . . . . 14 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟) ↔ 𝑧𝑟))
1691683expia 1111 . . . . . . . . . . . . 13 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → (𝑧𝐵 → ((¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟) ↔ 𝑧𝑟)))
170169pm5.32d 572 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ (𝑧𝐵𝑧𝑟)))
171124, 125orbi12i 901 . . . . . . . . . . . . 13 ((𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∨ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∨ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
172 elun 3975 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∨ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
173 andi 993 . . . . . . . . . . . . 13 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∨ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
174171, 172, 1733bitr4ri 296 . . . . . . . . . . . 12 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
175 eldifsn 4549 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐵 ∖ {𝑟}) ↔ (𝑧𝐵𝑧𝑟))
176175bicomi 216 . . . . . . . . . . . 12 ((𝑧𝐵𝑧𝑟) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟}))
177170, 174, 1763bitr3g 305 . . . . . . . . . . 11 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟})))
178160, 161, 162, 177eqrd 3839 . . . . . . . . . 10 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = (𝐵 ∖ {𝑟}))
179159, 145, 178syl2anc 579 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = (𝐵 ∖ {𝑟}))
180158, 179sseqtr4d 3860 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
181180adantlr 705 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
18224, 26, 66, 83, 103, 118, 144, 181nconnsubb 21635 . . . . . 6 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ¬ (𝐽t 𝐴) ∈ Conn)
183182anasss 460 . . . . 5 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Conn)
184183adantllr 709 . . . 4 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) ∧ 𝑟𝐵) ∧ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Conn)
185 rexanali 3178 . . . . . . . . . . 11 (∃𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
186185rexbii 3223 . . . . . . . . . 10 (∃𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑦𝐴 ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
187 rexcom 3284 . . . . . . . . . 10 (∃𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
188 rexnal 3175 . . . . . . . . . 10 (∃𝑦𝐴 ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
189186, 187, 1883bitr3i 293 . . . . . . . . 9 (∃𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
190189rexbii 3223 . . . . . . . 8 (∃𝑥𝐴𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑥𝐴 ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
191 rexcom 3284 . . . . . . . 8 (∃𝑥𝐴𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
192 rexnal 3175 . . . . . . . 8 (∃𝑥𝐴 ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
193190, 191, 1923bitr3i 293 . . . . . . 7 (∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
194 r19.41v 3274 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
195194rexbii 3223 . . . . . . . . 9 (∃𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑥𝐴 (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
196 r19.41v 3274 . . . . . . . . 9 (∃𝑥𝐴 (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ (∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
197 reeanv 3292 . . . . . . . . . 10 (∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ↔ (∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦))
198197anbi1i 617 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
199195, 196, 1983bitri 289 . . . . . . . 8 (∃𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
200199rexbii 3223 . . . . . . 7 (∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
201193, 200bitr3i 269 . . . . . 6 (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
20227ad2antrr 716 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝐾 ∈ Toset)
20325sselda 3820 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝐵)
204 simpllr 766 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑟𝐵)
20517, 10trleile 30228 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ 𝑥𝐵𝑟𝐵) → (𝑥 𝑟𝑟 𝑥))
206202, 203, 204, 205syl3anc 1439 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (𝑥 𝑟𝑟 𝑥))
207 simpr 479 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝐴)
208 simplr 759 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ¬ 𝑟𝐴)
209 nelne2 3067 . . . . . . . . . . . . . . 15 ((𝑥𝐴 ∧ ¬ 𝑟𝐴) → 𝑥𝑟)
210207, 208, 209syl2anc 579 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝑟)
211159adantr 474 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝐾 ∈ Poset)
21217, 10posrasymb 30219 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑥𝐵𝑟𝐵) → ((𝑥 𝑟𝑟 𝑥) ↔ 𝑥 = 𝑟))
213212necon3bbid 3005 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑥𝐵𝑟𝐵) → (¬ (𝑥 𝑟𝑟 𝑥) ↔ 𝑥𝑟))
214211, 203, 204, 213syl3anc 1439 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (¬ (𝑥 𝑟𝑟 𝑥) ↔ 𝑥𝑟))
215210, 214mpbird 249 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ¬ (𝑥 𝑟𝑟 𝑥))
216206, 215jca 507 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ((𝑥 𝑟𝑟 𝑥) ∧ ¬ (𝑥 𝑟𝑟 𝑥)))
217 pm5.17 997 . . . . . . . . . . . 12 (((𝑥 𝑟𝑟 𝑥) ∧ ¬ (𝑥 𝑟𝑟 𝑥)) ↔ (𝑥 𝑟 ↔ ¬ 𝑟 𝑥))
218216, 217sylib 210 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (𝑥 𝑟 ↔ ¬ 𝑟 𝑥))
219218rexbidva 3233 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (∃𝑥𝐴 𝑥 𝑟 ↔ ∃𝑥𝐴 ¬ 𝑟 𝑥))
22027ad2antrr 716 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝐾 ∈ Toset)
221 simpllr 766 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑟𝐵)
22225sselda 3820 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝐵)
22317, 10trleile 30228 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑦𝐵) → (𝑟 𝑦𝑦 𝑟))
224220, 221, 222, 223syl3anc 1439 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (𝑟 𝑦𝑦 𝑟))
225 simpr 479 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝐴)
226 simplr 759 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ¬ 𝑟𝐴)
227 nelne2 3067 . . . . . . . . . . . . . . . 16 ((𝑦𝐴 ∧ ¬ 𝑟𝐴) → 𝑦𝑟)
228225, 226, 227syl2anc 579 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝑟)
229228necomd 3023 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑟𝑦)
230159adantr 474 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝐾 ∈ Poset)
23117, 10posrasymb 30219 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑦𝐵) → ((𝑟 𝑦𝑦 𝑟) ↔ 𝑟 = 𝑦))
232231necon3bbid 3005 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑦𝐵) → (¬ (𝑟 𝑦𝑦 𝑟) ↔ 𝑟𝑦))
233230, 221, 222, 232syl3anc 1439 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (¬ (𝑟 𝑦𝑦 𝑟) ↔ 𝑟𝑦))
234229, 233mpbird 249 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ¬ (𝑟 𝑦𝑦 𝑟))
235224, 234jca 507 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ((𝑟 𝑦𝑦 𝑟) ∧ ¬ (𝑟 𝑦𝑦 𝑟)))
236 pm5.17 997 . . . . . . . . . . . 12 (((𝑟 𝑦𝑦 𝑟) ∧ ¬ (𝑟 𝑦𝑦 𝑟)) ↔ (𝑟 𝑦 ↔ ¬ 𝑦 𝑟))
237235, 236sylib 210 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (𝑟 𝑦 ↔ ¬ 𝑦 𝑟))
238237rexbidva 3233 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (∃𝑦𝐴 𝑟 𝑦 ↔ ∃𝑦𝐴 ¬ 𝑦 𝑟))
239219, 238anbi12d 624 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ↔ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)))
240239ex 403 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (¬ 𝑟𝐴 → ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ↔ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟))))
241240pm5.32rd 573 . . . . . . 7 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
242241rexbidva 3233 . . . . . 6 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
243201, 242syl5bb 275 . . . . 5 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
244243biimpa 470 . . . 4 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) → ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴))
2456, 184, 244r19.29af 3261 . . 3 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Conn)
246245ex 403 . 2 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) → ¬ (𝐽t 𝐴) ∈ Conn))
247246con4d 115 1 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → ((𝐽t 𝐴) ∈ Conn → ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 836  w3a 1071   = wceq 1601  wex 1823  wcel 2106  wne 2968  wral 3089  wrex 3090  {crab 3093  Vcvv 3397  cdif 3788  cun 3789  cin 3790  wss 3791  c0 4140  {csn 4397   class class class wbr 4886  cmpt 4965   × cxp 5353  dom cdm 5355  ran crn 5356  cfv 6135  (class class class)co 6922  ficfi 8604  Basecbs 16255  lecple 16345  t crest 16467  topGenctg 16484  ordTopcordt 16545   Proset cproset 17312  Posetcpo 17326  Tosetctos 17419  TopOnctopon 21122  Conncconn 21623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-en 8242  df-fin 8245  df-fi 8605  df-rest 16469  df-topgen 16490  df-ordt 16547  df-proset 17314  df-poset 17332  df-toset 17420  df-top 21106  df-topon 21123  df-bases 21158  df-cld 21231  df-conn 21624
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator