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 31853
Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 31854. See also reconnlem1 23970. (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 1920 . . . . 5 𝑟(𝐾 ∈ Toset ∧ 𝐴𝐵)
2 nfcv 2908 . . . . . . 7 𝑟𝐴
3 nfra2w 3153 . . . . . . 7 𝑟𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
42, 3nfralw 3151 . . . . . 6 𝑟𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
54nfn 1863 . . . . 5 𝑟 ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
61, 5nfan 1905 . . . 4 𝑟((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
7 tospos 18119 . . . . . . . . . 10 (𝐾 ∈ Toset → 𝐾 ∈ Poset)
8 posprs 18015 . . . . . . . . . 10 (𝐾 ∈ Poset → 𝐾 ∈ Proset )
9 ordtconn.j . . . . . . . . . . 11 𝐽 = (ordTop‘ )
10 ordtconn.l . . . . . . . . . . . . . 14 = ((le‘𝐾) ∩ (𝐵 × 𝐵))
11 fvex 6781 . . . . . . . . . . . . . . 15 (le‘𝐾) ∈ V
1211inex1 5244 . . . . . . . . . . . . . 14 ((le‘𝐾) ∩ (𝐵 × 𝐵)) ∈ V
1310, 12eqeltri 2836 . . . . . . . . . . . . 13 ∈ V
14 eqid 2739 . . . . . . . . . . . . . 14 dom = dom
1514ordttopon 22325 . . . . . . . . . . . . 13 ( ∈ V → (ordTop‘ ) ∈ (TopOn‘dom ))
1613, 15ax-mp 5 . . . . . . . . . . . 12 (ordTop‘ ) ∈ (TopOn‘dom )
17 ordtconn.x . . . . . . . . . . . . . 14 𝐵 = (Base‘𝐾)
1817, 10prsdm 31843 . . . . . . . . . . . . 13 (𝐾 ∈ Proset → dom = 𝐵)
1918fveq2d 6772 . . . . . . . . . . . 12 (𝐾 ∈ Proset → (TopOn‘dom ) = (TopOn‘𝐵))
2016, 19eleqtrid 2846 . . . . . . . . . . 11 (𝐾 ∈ Proset → (ordTop‘ ) ∈ (TopOn‘𝐵))
219, 20eqeltrid 2844 . . . . . . . . . 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 5357 . . . . . . . . . . . . . . . 16 {𝐵} ∈ V
3017fvexi 6782 . . . . . . . . . . . . . . . . . . 19 𝐵 ∈ V
3130mptex 7093 . . . . . . . . . . . . . . . . . 18 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∈ V
3231rnex 7746 . . . . . . . . . . . . . . . . 17 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∈ V
3330mptex 7093 . . . . . . . . . . . . . . . . . 18 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ∈ V
3433rnex 7746 . . . . . . . . . . . . . . . . 17 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ∈ V
3532, 34unex 7587 . . . . . . . . . . . . . . . 16 (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ∈ V
3629, 35unex 7587 . . . . . . . . . . . . . . 15 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ∈ V
37 ssfii 9139 . . . . . . . . . . . . . . 15 (({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ∈ V → ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))))
3836, 37ax-mp 5 . . . . . . . . . . . . . 14 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))
39 fvex 6781 . . . . . . . . . . . . . . 15 (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))) ∈ V
40 bastg 22097 . . . . . . . . . . . . . . 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 3934 . . . . . . . . . . . . 13 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))))
43 eqid 2739 . . . . . . . . . . . . . . 15 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) = ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
44 eqid 2739 . . . . . . . . . . . . . . 15 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) = ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
4517, 10, 43, 44ordtprsval 31847 . . . . . . . . . . . . . 14 (𝐾 ∈ Proset → (ordTop‘ ) = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))))
469, 45eqtrid 2791 . . . . . . . . . . . . 13 (𝐾 ∈ Proset → 𝐽 = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))))
4742, 46sseqtrrid 3978 . . . . . . . . . . . 12 (𝐾 ∈ Proset → ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ 𝐽)
4847unssbd 4126 . . . . . . . . . . 11 (𝐾 ∈ Proset → (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ⊆ 𝐽)
4928, 48syl 17 . . . . . . . . . 10 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ⊆ 𝐽)
5049unssbd 4126 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ⊆ 𝐽)
51 breq2 5082 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑟 𝑧𝑟 𝑦))
5251notbid 317 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (¬ 𝑟 𝑧 ↔ ¬ 𝑟 𝑦))
5352cbvrabv 3424 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦}
54 breq1 5081 . . . . . . . . . . . . . . 15 (𝑥 = 𝑟 → (𝑥 𝑦𝑟 𝑦))
5554notbid 317 . . . . . . . . . . . . . 14 (𝑥 = 𝑟 → (¬ 𝑥 𝑦 ↔ ¬ 𝑟 𝑦))
5655rabbidv 3412 . . . . . . . . . . . . 13 (𝑥 = 𝑟 → {𝑦𝐵 ∣ ¬ 𝑥 𝑦} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦})
5756rspceeqv 3575 . . . . . . . . . . . 12 ((𝑟𝐵 ∧ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦}) → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
5853, 57mpan2 687 . . . . . . . . . . 11 (𝑟𝐵 → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
5930rabex 5259 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ V
60 eqid 2739 . . . . . . . . . . . . 13 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) = (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
6160elrnmpt 5862 . . . . . . . . . . . 12 ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ V → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6259, 61ax-mp 5 . . . . . . . . . . 11 ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
6358, 62sylibr 233 . . . . . . . . . 10 (𝑟𝐵 → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6463adantl 481 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6550, 64sseldd 3926 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ 𝐽)
6665ad2antrr 722 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ 𝐽)
6749unssad 4125 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ⊆ 𝐽)
68 breq1 5081 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑧 𝑟𝑦 𝑟))
6968notbid 317 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (¬ 𝑧 𝑟 ↔ ¬ 𝑦 𝑟))
7069cbvrabv 3424 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟}
71 breq2 5082 . . . . . . . . . . . . . . 15 (𝑥 = 𝑟 → (𝑦 𝑥𝑦 𝑟))
7271notbid 317 . . . . . . . . . . . . . 14 (𝑥 = 𝑟 → (¬ 𝑦 𝑥 ↔ ¬ 𝑦 𝑟))
7372rabbidv 3412 . . . . . . . . . . . . 13 (𝑥 = 𝑟 → {𝑦𝐵 ∣ ¬ 𝑦 𝑥} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟})
7473rspceeqv 3575 . . . . . . . . . . . 12 ((𝑟𝐵 ∧ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟}) → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7570, 74mpan2 687 . . . . . . . . . . 11 (𝑟𝐵 → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7630rabex 5259 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ V
77 eqid 2739 . . . . . . . . . . . . 13 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) = (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7877elrnmpt 5862 . . . . . . . . . . . 12 ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ V → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
7976, 78ax-mp 5 . . . . . . . . . . 11 ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
8075, 79sylibr 233 . . . . . . . . . 10 (𝑟𝐵 → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
8180adantl 481 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
8267, 81sseldd 3926 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ 𝐽)
8382ad2antrr 722 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ 𝐽)
84 simpll 763 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵))
85 simpr 484 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ¬ 𝑟𝐴)
8684, 85jca 511 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴))
87 simplrl 773 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ∃𝑥𝐴 ¬ 𝑟 𝑥)
88 ssel 3918 . . . . . . . . . . . . . . 15 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
8988ancrd 551 . . . . . . . . . . . . . 14 (𝐴𝐵 → (𝑥𝐴 → (𝑥𝐵𝑥𝐴)))
9089anim1d 610 . . . . . . . . . . . . 13 (𝐴𝐵 → ((𝑥𝐴 ∧ ¬ 𝑟 𝑥) → ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥)))
9190impl 455 . . . . . . . . . . . 12 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
92 elin 3907 . . . . . . . . . . . . 13 (𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ↔ (𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑥𝐴))
93 breq2 5082 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑥 → (𝑟 𝑧𝑟 𝑥))
9493notbid 317 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → (¬ 𝑟 𝑧 ↔ ¬ 𝑟 𝑥))
9594elrab 3625 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ↔ (𝑥𝐵 ∧ ¬ 𝑟 𝑥))
9695anbi1i 623 . . . . . . . . . . . . 13 ((𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑥𝐴) ↔ ((𝑥𝐵 ∧ ¬ 𝑟 𝑥) ∧ 𝑥𝐴))
97 an32 642 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ¬ 𝑟 𝑥) ∧ 𝑥𝐴) ↔ ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
9892, 96, 973bitri 296 . . . . . . . . . . . 12 (𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ↔ ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
9991, 98sylibr 233 . . . . . . . . . . 11 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → 𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴))
10099ne0d 4274 . . . . . . . . . 10 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
10125, 100sylanl1 676 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
102101r19.29an 3218 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ ∃𝑥𝐴 ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
10386, 87, 102syl2anc 583 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
104 simplrr 774 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ∃𝑦𝐴 ¬ 𝑦 𝑟)
105 ssel 3918 . . . . . . . . . . . . . . 15 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
106105ancrd 551 . . . . . . . . . . . . . 14 (𝐴𝐵 → (𝑦𝐴 → (𝑦𝐵𝑦𝐴)))
107106anim1d 610 . . . . . . . . . . . . 13 (𝐴𝐵 → ((𝑦𝐴 ∧ ¬ 𝑦 𝑟) → ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟)))
108107impl 455 . . . . . . . . . . . 12 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
109 elin 3907 . . . . . . . . . . . . 13 (𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ↔ (𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∧ 𝑦𝐴))
11069elrab 3625 . . . . . . . . . . . . . 14 (𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ↔ (𝑦𝐵 ∧ ¬ 𝑦 𝑟))
111110anbi1i 623 . . . . . . . . . . . . 13 ((𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∧ 𝑦𝐴) ↔ ((𝑦𝐵 ∧ ¬ 𝑦 𝑟) ∧ 𝑦𝐴))
112 an32 642 . . . . . . . . . . . . 13 (((𝑦𝐵 ∧ ¬ 𝑦 𝑟) ∧ 𝑦𝐴) ↔ ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
113109, 111, 1123bitri 296 . . . . . . . . . . . 12 (𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ↔ ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
114108, 113sylibr 233 . . . . . . . . . . 11 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → 𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴))
115114ne0d 4274 . . . . . . . . . 10 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
11625, 115sylanl1 676 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
117116r19.29an 3218 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
11886, 104, 117syl2anc 583 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
11917, 10trleile 31228 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑧𝐵) → (𝑟 𝑧𝑧 𝑟))
120 oran 986 . . . . . . . . . . . . . . . 16 ((𝑟 𝑧𝑧 𝑟) ↔ ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
121119, 120sylib 217 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑧𝐵) → ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
1221213expa 1116 . . . . . . . . . . . . . 14 (((𝐾 ∈ Toset ∧ 𝑟𝐵) ∧ 𝑧𝐵) → ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
123122nrexdv 3199 . . . . . . . . . . . . 13 ((𝐾 ∈ Toset ∧ 𝑟𝐵) → ¬ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
124 rabid 3308 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ↔ (𝑧𝐵 ∧ ¬ 𝑟 𝑧))
125 rabid 3308 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ↔ (𝑧𝐵 ∧ ¬ 𝑧 𝑟))
126124, 125anbi12i 626 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∧ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
127 elin 3907 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
128 anandi 672 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∧ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
129126, 127, 1283bitr4i 302 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
130129exbii 1853 . . . . . . . . . . . . . . 15 (∃𝑧 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ∃𝑧(𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
131 nfrab1 3315 . . . . . . . . . . . . . . . . 17 𝑧{𝑧𝐵 ∣ ¬ 𝑟 𝑧}
132 nfrab1 3315 . . . . . . . . . . . . . . . . 17 𝑧{𝑧𝐵 ∣ ¬ 𝑧 𝑟}
133131, 132nfin 4155 . . . . . . . . . . . . . . . 16 𝑧({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟})
134133n0f 4281 . . . . . . . . . . . . . . 15 (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
135 df-rex 3071 . . . . . . . . . . . . . . 15 (∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟) ↔ ∃𝑧(𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
136130, 134, 1353bitr4i 302 . . . . . . . . . . . . . 14 (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ≠ ∅ ↔ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
137136necon1bbii 2994 . . . . . . . . . . . . 13 (¬ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟) ↔ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
138123, 137sylib 217 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
139138adantlr 711 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
140139adantr 480 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
141140ineq1d 4150 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = (∅ ∩ 𝐴))
142 0in 4332 . . . . . . . . 9 (∅ ∩ 𝐴) = ∅
143141, 142eqtrdi 2795 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = ∅)
144143adantlr 711 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = ∅)
145 simplr 765 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝑟𝐵)
146 simpr 484 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ¬ 𝑟𝐴)
147 vex 3434 . . . . . . . . . . . . . . 15 𝑟 ∈ V
148147snss 4724 . . . . . . . . . . . . . 14 (𝑟𝐵 ↔ {𝑟} ⊆ 𝐵)
149 eldif 3901 . . . . . . . . . . . . . . . 16 (𝑟 ∈ (𝐵𝐴) ↔ (𝑟𝐵 ∧ ¬ 𝑟𝐴))
150147snss 4724 . . . . . . . . . . . . . . . 16 (𝑟 ∈ (𝐵𝐴) ↔ {𝑟} ⊆ (𝐵𝐴))
151149, 150bitr3i 276 . . . . . . . . . . . . . . 15 ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ {𝑟} ⊆ (𝐵𝐴))
152 ssconb 4076 . . . . . . . . . . . . . . 15 (({𝑟} ⊆ 𝐵𝐴𝐵) → ({𝑟} ⊆ (𝐵𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
153151, 152syl5bb 282 . . . . . . . . . . . . . 14 (({𝑟} ⊆ 𝐵𝐴𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
154148, 153sylanb 580 . . . . . . . . . . . . 13 ((𝑟𝐵𝐴𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
155154adantl 481 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ (𝑟𝐵𝐴𝐵)) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
156155anass1rs 651 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
157156adantr 480 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
158145, 146, 157mpbi2and 708 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ (𝐵 ∖ {𝑟}))
1597ad3antrrr 726 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐾 ∈ Poset)
160 nfv 1920 . . . . . . . . . . 11 𝑧(𝐾 ∈ Poset ∧ 𝑟𝐵)
161131, 132nfun 4103 . . . . . . . . . . 11 𝑧({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟})
162 nfcv 2908 . . . . . . . . . . 11 𝑧(𝐵 ∖ {𝑟})
163 ianor 978 . . . . . . . . . . . . . . 15 (¬ (𝑟 𝑧𝑧 𝑟) ↔ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟))
16417, 10posrasymb 31222 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((𝑟 𝑧𝑧 𝑟) ↔ 𝑟 = 𝑧))
165 equcom 2024 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑧𝑧 = 𝑟)
166164, 165bitrdi 286 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((𝑟 𝑧𝑧 𝑟) ↔ 𝑧 = 𝑟))
167166necon3bbid 2982 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → (¬ (𝑟 𝑧𝑧 𝑟) ↔ 𝑧𝑟))
168163, 167bitr3id 284 . . . . . . . . . . . . . 14 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟) ↔ 𝑧𝑟))
1691683expia 1119 . . . . . . . . . . . . 13 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → (𝑧𝐵 → ((¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟) ↔ 𝑧𝑟)))
170169pm5.32d 576 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ (𝑧𝐵𝑧𝑟)))
171124, 125orbi12i 911 . . . . . . . . . . . . 13 ((𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∨ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∨ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
172 elun 4087 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∨ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
173 andi 1004 . . . . . . . . . . . . 13 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∨ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
174171, 172, 1733bitr4ri 303 . . . . . . . . . . . 12 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
175 eldifsn 4725 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐵 ∖ {𝑟}) ↔ (𝑧𝐵𝑧𝑟))
176175bicomi 223 . . . . . . . . . . . 12 ((𝑧𝐵𝑧𝑟) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟}))
177170, 174, 1763bitr3g 312 . . . . . . . . . . 11 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟})))
178160, 161, 162, 177eqrd 3944 . . . . . . . . . 10 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = (𝐵 ∖ {𝑟}))
179159, 145, 178syl2anc 583 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = (𝐵 ∖ {𝑟}))
180158, 179sseqtrrd 3966 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
181180adantlr 711 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
18224, 26, 66, 83, 103, 118, 144, 181nconnsubb 22555 . . . . . 6 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ¬ (𝐽t 𝐴) ∈ Conn)
183182anasss 466 . . . . 5 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Conn)
184183adantllr 715 . . . 4 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) ∧ 𝑟𝐵) ∧ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Conn)
185 rexanali 3193 . . . . . . . . . . 11 (∃𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
186185rexbii 3179 . . . . . . . . . 10 (∃𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑦𝐴 ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
187 rexcom 3283 . . . . . . . . . 10 (∃𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
188 rexnal 3167 . . . . . . . . . 10 (∃𝑦𝐴 ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
189186, 187, 1883bitr3i 300 . . . . . . . . 9 (∃𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
190189rexbii 3179 . . . . . . . 8 (∃𝑥𝐴𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑥𝐴 ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
191 rexcom 3283 . . . . . . . 8 (∃𝑥𝐴𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
192 rexnal 3167 . . . . . . . 8 (∃𝑥𝐴 ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
193190, 191, 1923bitr3i 300 . . . . . . 7 (∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
194 r19.41v 3275 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
195194rexbii 3179 . . . . . . . . 9 (∃𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑥𝐴 (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
196 r19.41v 3275 . . . . . . . . 9 (∃𝑥𝐴 (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ (∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
197 reeanv 3294 . . . . . . . . . 10 (∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ↔ (∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦))
198197anbi1i 623 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
199195, 196, 1983bitri 296 . . . . . . . 8 (∃𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
200199rexbii 3179 . . . . . . 7 (∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
201193, 200bitr3i 276 . . . . . 6 (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
20227ad2antrr 722 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝐾 ∈ Toset)
20325sselda 3925 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝐵)
204 simpllr 772 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑟𝐵)
20517, 10trleile 31228 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ 𝑥𝐵𝑟𝐵) → (𝑥 𝑟𝑟 𝑥))
206202, 203, 204, 205syl3anc 1369 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (𝑥 𝑟𝑟 𝑥))
207 simpr 484 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝐴)
208 simplr 765 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ¬ 𝑟𝐴)
209 nelne2 3043 . . . . . . . . . . . . . . 15 ((𝑥𝐴 ∧ ¬ 𝑟𝐴) → 𝑥𝑟)
210207, 208, 209syl2anc 583 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝑟)
211159adantr 480 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝐾 ∈ Poset)
21217, 10posrasymb 31222 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑥𝐵𝑟𝐵) → ((𝑥 𝑟𝑟 𝑥) ↔ 𝑥 = 𝑟))
213212necon3bbid 2982 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑥𝐵𝑟𝐵) → (¬ (𝑥 𝑟𝑟 𝑥) ↔ 𝑥𝑟))
214211, 203, 204, 213syl3anc 1369 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (¬ (𝑥 𝑟𝑟 𝑥) ↔ 𝑥𝑟))
215210, 214mpbird 256 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ¬ (𝑥 𝑟𝑟 𝑥))
216206, 215jca 511 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ((𝑥 𝑟𝑟 𝑥) ∧ ¬ (𝑥 𝑟𝑟 𝑥)))
217 pm5.17 1008 . . . . . . . . . . . 12 (((𝑥 𝑟𝑟 𝑥) ∧ ¬ (𝑥 𝑟𝑟 𝑥)) ↔ (𝑥 𝑟 ↔ ¬ 𝑟 𝑥))
218216, 217sylib 217 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (𝑥 𝑟 ↔ ¬ 𝑟 𝑥))
219218rexbidva 3226 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (∃𝑥𝐴 𝑥 𝑟 ↔ ∃𝑥𝐴 ¬ 𝑟 𝑥))
22027ad2antrr 722 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝐾 ∈ Toset)
221 simpllr 772 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑟𝐵)
22225sselda 3925 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝐵)
22317, 10trleile 31228 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑦𝐵) → (𝑟 𝑦𝑦 𝑟))
224220, 221, 222, 223syl3anc 1369 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (𝑟 𝑦𝑦 𝑟))
225 simpr 484 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝐴)
226 simplr 765 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ¬ 𝑟𝐴)
227 nelne2 3043 . . . . . . . . . . . . . . . 16 ((𝑦𝐴 ∧ ¬ 𝑟𝐴) → 𝑦𝑟)
228225, 226, 227syl2anc 583 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝑟)
229228necomd 3000 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑟𝑦)
230159adantr 480 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝐾 ∈ Poset)
23117, 10posrasymb 31222 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑦𝐵) → ((𝑟 𝑦𝑦 𝑟) ↔ 𝑟 = 𝑦))
232231necon3bbid 2982 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑦𝐵) → (¬ (𝑟 𝑦𝑦 𝑟) ↔ 𝑟𝑦))
233230, 221, 222, 232syl3anc 1369 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (¬ (𝑟 𝑦𝑦 𝑟) ↔ 𝑟𝑦))
234229, 233mpbird 256 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ¬ (𝑟 𝑦𝑦 𝑟))
235224, 234jca 511 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ((𝑟 𝑦𝑦 𝑟) ∧ ¬ (𝑟 𝑦𝑦 𝑟)))
236 pm5.17 1008 . . . . . . . . . . . 12 (((𝑟 𝑦𝑦 𝑟) ∧ ¬ (𝑟 𝑦𝑦 𝑟)) ↔ (𝑟 𝑦 ↔ ¬ 𝑦 𝑟))
237235, 236sylib 217 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (𝑟 𝑦 ↔ ¬ 𝑦 𝑟))
238237rexbidva 3226 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (∃𝑦𝐴 𝑟 𝑦 ↔ ∃𝑦𝐴 ¬ 𝑦 𝑟))
239219, 238anbi12d 630 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ↔ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)))
240239ex 412 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (¬ 𝑟𝐴 → ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ↔ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟))))
241240pm5.32rd 577 . . . . . . 7 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
242241rexbidva 3226 . . . . . 6 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
243201, 242syl5bb 282 . . . . 5 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
244243biimpa 476 . . . 4 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) → ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴))
2456, 184, 244r19.29af 3261 . . 3 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Conn)
246245ex 412 . 2 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) → ¬ (𝐽t 𝐴) ∈ Conn))
247246con4d 115 1 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → ((𝐽t 𝐴) ∈ Conn → ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 843  w3a 1085   = wceq 1541  wex 1785  wcel 2109  wne 2944  wral 3065  wrex 3066  {crab 3069  Vcvv 3430  cdif 3888  cun 3889  cin 3890  wss 3891  c0 4261  {csn 4566   class class class wbr 5078  cmpt 5161   × cxp 5586  dom cdm 5588  ran crn 5589  cfv 6430  (class class class)co 7268  ficfi 9130  Basecbs 16893  lecple 16950  t crest 17112  topGenctg 17129  ordTopcordt 17191   Proset cproset 17992  Posetcpo 18006  Tosetctos 18115  TopOnctopon 22040  Conncconn 22543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-rep 5213  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-int 4885  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-ov 7271  df-oprab 7272  df-mpo 7273  df-om 7701  df-1st 7817  df-2nd 7818  df-1o 8281  df-er 8472  df-en 8708  df-fin 8711  df-fi 9131  df-rest 17114  df-topgen 17135  df-ordt 17193  df-proset 17994  df-poset 18012  df-toset 18116  df-top 22024  df-topon 22041  df-bases 22077  df-cld 22151  df-conn 22544
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator