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 30420
Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 30421. See also reconnlem1 22911. (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 2009 . . . . 5 𝑟(𝐾 ∈ Toset ∧ 𝐴𝐵)
2 nfcv 2907 . . . . . . 7 𝑟𝐴
3 nfra2 3093 . . . . . . 7 𝑟𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
42, 3nfral 3092 . . . . . 6 𝑟𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
54nfn 1953 . . . . 5 𝑟 ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
61, 5nfan 1998 . . . 4 𝑟((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
7 tospos 30108 . . . . . . . . . 10 (𝐾 ∈ Toset → 𝐾 ∈ Poset)
8 posprs 17218 . . . . . . . . . 10 (𝐾 ∈ Poset → 𝐾 ∈ Proset )
9 ordtconn.j . . . . . . . . . . 11 𝐽 = (ordTop‘ )
10 ordtconn.l . . . . . . . . . . . . . 14 = ((le‘𝐾) ∩ (𝐵 × 𝐵))
11 fvex 6390 . . . . . . . . . . . . . . 15 (le‘𝐾) ∈ V
1211inex1 4962 . . . . . . . . . . . . . 14 ((le‘𝐾) ∩ (𝐵 × 𝐵)) ∈ V
1310, 12eqeltri 2840 . . . . . . . . . . . . 13 ∈ V
14 eqid 2765 . . . . . . . . . . . . . 14 dom = dom
1514ordttopon 21280 . . . . . . . . . . . . 13 ( ∈ V → (ordTop‘ ) ∈ (TopOn‘dom ))
1613, 15ax-mp 5 . . . . . . . . . . . 12 (ordTop‘ ) ∈ (TopOn‘dom )
17 ordtconn.x . . . . . . . . . . . . . 14 𝐵 = (Base‘𝐾)
1817, 10prsdm 30410 . . . . . . . . . . . . 13 (𝐾 ∈ Proset → dom = 𝐵)
1918fveq2d 6381 . . . . . . . . . . . 12 (𝐾 ∈ Proset → (TopOn‘dom ) = (TopOn‘𝐵))
2016, 19syl5eleq 2850 . . . . . . . . . . 11 (𝐾 ∈ Proset → (ordTop‘ ) ∈ (TopOn‘𝐵))
219, 20syl5eqel 2848 . . . . . . . . . 10 (𝐾 ∈ Proset → 𝐽 ∈ (TopOn‘𝐵))
227, 8, 213syl 18 . . . . . . . . 9 (𝐾 ∈ Toset → 𝐽 ∈ (TopOn‘𝐵))
2322ad3antrrr 721 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐽 ∈ (TopOn‘𝐵))
2423adantlr 706 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → 𝐽 ∈ (TopOn‘𝐵))
25 simpllr 793 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴𝐵)
2625adantlr 706 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → 𝐴𝐵)
27 simpll 783 . . . . . . . . . . . 12 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → 𝐾 ∈ Toset)
2827, 7, 83syl 18 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → 𝐾 ∈ Proset )
29 snex 5066 . . . . . . . . . . . . . . . 16 {𝐵} ∈ V
3017fvexi 6391 . . . . . . . . . . . . . . . . . . 19 𝐵 ∈ V
3130mptex 6681 . . . . . . . . . . . . . . . . . 18 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∈ V
3231rnex 7300 . . . . . . . . . . . . . . . . 17 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∈ V
3330mptex 6681 . . . . . . . . . . . . . . . . . 18 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ∈ V
3433rnex 7300 . . . . . . . . . . . . . . . . 17 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ∈ V
3532, 34unex 7156 . . . . . . . . . . . . . . . 16 (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ∈ V
3629, 35unex 7156 . . . . . . . . . . . . . . 15 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ∈ V
37 ssfii 8534 . . . . . . . . . . . . . . 15 (({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ∈ V → ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))))
3836, 37ax-mp 5 . . . . . . . . . . . . . 14 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))
39 fvex 6390 . . . . . . . . . . . . . . 15 (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))) ∈ V
40 bastg 21053 . . . . . . . . . . . . . . 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 3772 . . . . . . . . . . . . 13 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))))
43 eqid 2765 . . . . . . . . . . . . . . 15 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) = ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
44 eqid 2765 . . . . . . . . . . . . . . 15 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) = ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
4517, 10, 43, 44ordtprsval 30414 . . . . . . . . . . . . . 14 (𝐾 ∈ Proset → (ordTop‘ ) = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))))
469, 45syl5eq 2811 . . . . . . . . . . . . 13 (𝐾 ∈ Proset → 𝐽 = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))))
4742, 46syl5sseqr 3816 . . . . . . . . . . . 12 (𝐾 ∈ Proset → ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ 𝐽)
4847unssbd 3955 . . . . . . . . . . 11 (𝐾 ∈ Proset → (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ⊆ 𝐽)
4928, 48syl 17 . . . . . . . . . 10 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ⊆ 𝐽)
5049unssbd 3955 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ⊆ 𝐽)
51 breq2 4815 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑟 𝑧𝑟 𝑦))
5251notbid 309 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (¬ 𝑟 𝑧 ↔ ¬ 𝑟 𝑦))
5352cbvrabv 3348 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦}
54 breq1 4814 . . . . . . . . . . . . . . 15 (𝑥 = 𝑟 → (𝑥 𝑦𝑟 𝑦))
5554notbid 309 . . . . . . . . . . . . . 14 (𝑥 = 𝑟 → (¬ 𝑥 𝑦 ↔ ¬ 𝑟 𝑦))
5655rabbidv 3338 . . . . . . . . . . . . 13 (𝑥 = 𝑟 → {𝑦𝐵 ∣ ¬ 𝑥 𝑦} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦})
5756rspceeqv 3480 . . . . . . . . . . . 12 ((𝑟𝐵 ∧ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦}) → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
5853, 57mpan2 682 . . . . . . . . . . 11 (𝑟𝐵 → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
5930rabex 4975 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ V
60 eqid 2765 . . . . . . . . . . . . 13 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) = (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
6160elrnmpt 5543 . . . . . . . . . . . 12 ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ V → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6259, 61ax-mp 5 . . . . . . . . . . 11 ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
6358, 62sylibr 225 . . . . . . . . . 10 (𝑟𝐵 → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6463adantl 473 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6550, 64sseldd 3764 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ 𝐽)
6665ad2antrr 717 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ 𝐽)
6749unssad 3954 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ⊆ 𝐽)
68 breq1 4814 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑧 𝑟𝑦 𝑟))
6968notbid 309 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (¬ 𝑧 𝑟 ↔ ¬ 𝑦 𝑟))
7069cbvrabv 3348 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟}
71 breq2 4815 . . . . . . . . . . . . . . 15 (𝑥 = 𝑟 → (𝑦 𝑥𝑦 𝑟))
7271notbid 309 . . . . . . . . . . . . . 14 (𝑥 = 𝑟 → (¬ 𝑦 𝑥 ↔ ¬ 𝑦 𝑟))
7372rabbidv 3338 . . . . . . . . . . . . 13 (𝑥 = 𝑟 → {𝑦𝐵 ∣ ¬ 𝑦 𝑥} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟})
7473rspceeqv 3480 . . . . . . . . . . . 12 ((𝑟𝐵 ∧ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟}) → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7570, 74mpan2 682 . . . . . . . . . . 11 (𝑟𝐵 → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7630rabex 4975 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ V
77 eqid 2765 . . . . . . . . . . . . 13 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) = (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7877elrnmpt 5543 . . . . . . . . . . . 12 ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ V → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
7976, 78ax-mp 5 . . . . . . . . . . 11 ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
8075, 79sylibr 225 . . . . . . . . . 10 (𝑟𝐵 → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
8180adantl 473 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
8267, 81sseldd 3764 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ 𝐽)
8382ad2antrr 717 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ 𝐽)
84 simpll 783 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵))
85 simpr 477 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ¬ 𝑟𝐴)
8684, 85jca 507 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴))
87 simplrl 795 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ∃𝑥𝐴 ¬ 𝑟 𝑥)
88 ssel 3757 . . . . . . . . . . . . . . 15 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
8988ancrd 547 . . . . . . . . . . . . . 14 (𝐴𝐵 → (𝑥𝐴 → (𝑥𝐵𝑥𝐴)))
9089anim1d 604 . . . . . . . . . . . . 13 (𝐴𝐵 → ((𝑥𝐴 ∧ ¬ 𝑟 𝑥) → ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥)))
9190impl 447 . . . . . . . . . . . 12 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
92 elin 3960 . . . . . . . . . . . . 13 (𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ↔ (𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑥𝐴))
93 breq2 4815 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑥 → (𝑟 𝑧𝑟 𝑥))
9493notbid 309 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → (¬ 𝑟 𝑧 ↔ ¬ 𝑟 𝑥))
9594elrab 3521 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ↔ (𝑥𝐵 ∧ ¬ 𝑟 𝑥))
9695anbi1i 617 . . . . . . . . . . . . 13 ((𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑥𝐴) ↔ ((𝑥𝐵 ∧ ¬ 𝑟 𝑥) ∧ 𝑥𝐴))
97 an32 636 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ¬ 𝑟 𝑥) ∧ 𝑥𝐴) ↔ ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
9892, 96, 973bitri 288 . . . . . . . . . . . 12 (𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ↔ ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
9991, 98sylibr 225 . . . . . . . . . . 11 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → 𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴))
10099ne0d 4088 . . . . . . . . . 10 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
10125, 100sylanl1 670 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
102101r19.29an 3224 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ ∃𝑥𝐴 ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
10386, 87, 102syl2anc 579 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
104 simplrr 796 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ∃𝑦𝐴 ¬ 𝑦 𝑟)
105 ssel 3757 . . . . . . . . . . . . . . 15 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
106105ancrd 547 . . . . . . . . . . . . . 14 (𝐴𝐵 → (𝑦𝐴 → (𝑦𝐵𝑦𝐴)))
107106anim1d 604 . . . . . . . . . . . . 13 (𝐴𝐵 → ((𝑦𝐴 ∧ ¬ 𝑦 𝑟) → ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟)))
108107impl 447 . . . . . . . . . . . 12 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
109 elin 3960 . . . . . . . . . . . . 13 (𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ↔ (𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∧ 𝑦𝐴))
11069elrab 3521 . . . . . . . . . . . . . 14 (𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ↔ (𝑦𝐵 ∧ ¬ 𝑦 𝑟))
111110anbi1i 617 . . . . . . . . . . . . 13 ((𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∧ 𝑦𝐴) ↔ ((𝑦𝐵 ∧ ¬ 𝑦 𝑟) ∧ 𝑦𝐴))
112 an32 636 . . . . . . . . . . . . 13 (((𝑦𝐵 ∧ ¬ 𝑦 𝑟) ∧ 𝑦𝐴) ↔ ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
113109, 111, 1123bitri 288 . . . . . . . . . . . 12 (𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ↔ ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
114108, 113sylibr 225 . . . . . . . . . . 11 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → 𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴))
115114ne0d 4088 . . . . . . . . . 10 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
11625, 115sylanl1 670 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
117116r19.29an 3224 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
11886, 104, 117syl2anc 579 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
11917, 10trleile 30116 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑧𝐵) → (𝑟 𝑧𝑧 𝑟))
120 oran 1012 . . . . . . . . . . . . . . . 16 ((𝑟 𝑧𝑧 𝑟) ↔ ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
121119, 120sylib 209 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑧𝐵) → ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
1221213expa 1147 . . . . . . . . . . . . . 14 (((𝐾 ∈ Toset ∧ 𝑟𝐵) ∧ 𝑧𝐵) → ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
123122nrexdv 3147 . . . . . . . . . . . . 13 ((𝐾 ∈ Toset ∧ 𝑟𝐵) → ¬ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
124 rabid 3263 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ↔ (𝑧𝐵 ∧ ¬ 𝑟 𝑧))
125 rabid 3263 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ↔ (𝑧𝐵 ∧ ¬ 𝑧 𝑟))
126124, 125anbi12i 620 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∧ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
127 elin 3960 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
128 anandi 666 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∧ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
129126, 127, 1283bitr4i 294 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
130129exbii 1943 . . . . . . . . . . . . . . 15 (∃𝑧 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ∃𝑧(𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
131 nfrab1 3270 . . . . . . . . . . . . . . . . 17 𝑧{𝑧𝐵 ∣ ¬ 𝑟 𝑧}
132 nfrab1 3270 . . . . . . . . . . . . . . . . 17 𝑧{𝑧𝐵 ∣ ¬ 𝑧 𝑟}
133131, 132nfin 3982 . . . . . . . . . . . . . . . 16 𝑧({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟})
134133n0f 4094 . . . . . . . . . . . . . . 15 (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
135 df-rex 3061 . . . . . . . . . . . . . . 15 (∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟) ↔ ∃𝑧(𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
136130, 134, 1353bitr4i 294 . . . . . . . . . . . . . 14 (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ≠ ∅ ↔ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
137136necon1bbii 2986 . . . . . . . . . . . . 13 (¬ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟) ↔ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
138123, 137sylib 209 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
139138adantlr 706 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
140139adantr 472 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
141140ineq1d 3977 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = (∅ ∩ 𝐴))
142 0in 4133 . . . . . . . . 9 (∅ ∩ 𝐴) = ∅
143141, 142syl6eq 2815 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = ∅)
144143adantlr 706 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = ∅)
145 simplr 785 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝑟𝐵)
146 simpr 477 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ¬ 𝑟𝐴)
147 vex 3353 . . . . . . . . . . . . . . 15 𝑟 ∈ V
148147snss 4472 . . . . . . . . . . . . . 14 (𝑟𝐵 ↔ {𝑟} ⊆ 𝐵)
149 eldif 3744 . . . . . . . . . . . . . . . 16 (𝑟 ∈ (𝐵𝐴) ↔ (𝑟𝐵 ∧ ¬ 𝑟𝐴))
150147snss 4472 . . . . . . . . . . . . . . . 16 (𝑟 ∈ (𝐵𝐴) ↔ {𝑟} ⊆ (𝐵𝐴))
151149, 150bitr3i 268 . . . . . . . . . . . . . . 15 ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ {𝑟} ⊆ (𝐵𝐴))
152 ssconb 3907 . . . . . . . . . . . . . . 15 (({𝑟} ⊆ 𝐵𝐴𝐵) → ({𝑟} ⊆ (𝐵𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
153151, 152syl5bb 274 . . . . . . . . . . . . . 14 (({𝑟} ⊆ 𝐵𝐴𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
154148, 153sylanb 576 . . . . . . . . . . . . 13 ((𝑟𝐵𝐴𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
155154adantl 473 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ (𝑟𝐵𝐴𝐵)) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
156155anass1rs 645 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
157156adantr 472 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
158145, 146, 157mpbi2and 703 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ (𝐵 ∖ {𝑟}))
1597ad3antrrr 721 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐾 ∈ Poset)
160 nfv 2009 . . . . . . . . . . 11 𝑧(𝐾 ∈ Poset ∧ 𝑟𝐵)
161131, 132nfun 3933 . . . . . . . . . . 11 𝑧({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟})
162 nfcv 2907 . . . . . . . . . . 11 𝑧(𝐵 ∖ {𝑟})
163 ianor 1004 . . . . . . . . . . . . . . 15 (¬ (𝑟 𝑧𝑧 𝑟) ↔ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟))
16417, 10posrasymb 30107 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((𝑟 𝑧𝑧 𝑟) ↔ 𝑟 = 𝑧))
165 equcom 2115 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑧𝑧 = 𝑟)
166164, 165syl6bb 278 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((𝑟 𝑧𝑧 𝑟) ↔ 𝑧 = 𝑟))
167166necon3bbid 2974 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → (¬ (𝑟 𝑧𝑧 𝑟) ↔ 𝑧𝑟))
168163, 167syl5bbr 276 . . . . . . . . . . . . . 14 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟) ↔ 𝑧𝑟))
1691683expia 1150 . . . . . . . . . . . . 13 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → (𝑧𝐵 → ((¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟) ↔ 𝑧𝑟)))
170169pm5.32d 572 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ (𝑧𝐵𝑧𝑟)))
171124, 125orbi12i 938 . . . . . . . . . . . . 13 ((𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∨ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∨ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
172 elun 3917 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∨ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
173 andi 1030 . . . . . . . . . . . . 13 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∨ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
174171, 172, 1733bitr4ri 295 . . . . . . . . . . . 12 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
175 eldifsn 4474 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐵 ∖ {𝑟}) ↔ (𝑧𝐵𝑧𝑟))
176175bicomi 215 . . . . . . . . . . . 12 ((𝑧𝐵𝑧𝑟) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟}))
177170, 174, 1763bitr3g 304 . . . . . . . . . . 11 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟})))
178160, 161, 162, 177eqrd 3782 . . . . . . . . . 10 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = (𝐵 ∖ {𝑟}))
179159, 145, 178syl2anc 579 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = (𝐵 ∖ {𝑟}))
180158, 179sseqtr4d 3804 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
181180adantlr 706 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
18224, 26, 66, 83, 103, 118, 144, 181nconnsubb 21509 . . . . . 6 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ¬ (𝐽t 𝐴) ∈ Conn)
183182anasss 458 . . . . 5 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Conn)
184183adantllr 710 . . . 4 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) ∧ 𝑟𝐵) ∧ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Conn)
185 rexanali 3144 . . . . . . . . . . 11 (∃𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
186185rexbii 3188 . . . . . . . . . 10 (∃𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑦𝐴 ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
187 rexcom 3246 . . . . . . . . . 10 (∃𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
188 rexnal 3141 . . . . . . . . . 10 (∃𝑦𝐴 ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
189186, 187, 1883bitr3i 292 . . . . . . . . 9 (∃𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
190189rexbii 3188 . . . . . . . 8 (∃𝑥𝐴𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑥𝐴 ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
191 rexcom 3246 . . . . . . . 8 (∃𝑥𝐴𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
192 rexnal 3141 . . . . . . . 8 (∃𝑥𝐴 ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
193190, 191, 1923bitr3i 292 . . . . . . 7 (∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
194 r19.41v 3236 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
195194rexbii 3188 . . . . . . . . 9 (∃𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑥𝐴 (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
196 r19.41v 3236 . . . . . . . . 9 (∃𝑥𝐴 (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ (∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
197 reeanv 3254 . . . . . . . . . 10 (∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ↔ (∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦))
198197anbi1i 617 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
199195, 196, 1983bitri 288 . . . . . . . 8 (∃𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
200199rexbii 3188 . . . . . . 7 (∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
201193, 200bitr3i 268 . . . . . 6 (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
20227ad2antrr 717 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝐾 ∈ Toset)
20325sselda 3763 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝐵)
204 simpllr 793 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑟𝐵)
20517, 10trleile 30116 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ 𝑥𝐵𝑟𝐵) → (𝑥 𝑟𝑟 𝑥))
206202, 203, 204, 205syl3anc 1490 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (𝑥 𝑟𝑟 𝑥))
207 simpr 477 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝐴)
208 simplr 785 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ¬ 𝑟𝐴)
209 nelne2 3034 . . . . . . . . . . . . . . 15 ((𝑥𝐴 ∧ ¬ 𝑟𝐴) → 𝑥𝑟)
210207, 208, 209syl2anc 579 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝑟)
211159adantr 472 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝐾 ∈ Poset)
21217, 10posrasymb 30107 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑥𝐵𝑟𝐵) → ((𝑥 𝑟𝑟 𝑥) ↔ 𝑥 = 𝑟))
213212necon3bbid 2974 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑥𝐵𝑟𝐵) → (¬ (𝑥 𝑟𝑟 𝑥) ↔ 𝑥𝑟))
214211, 203, 204, 213syl3anc 1490 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (¬ (𝑥 𝑟𝑟 𝑥) ↔ 𝑥𝑟))
215210, 214mpbird 248 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ¬ (𝑥 𝑟𝑟 𝑥))
216206, 215jca 507 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ((𝑥 𝑟𝑟 𝑥) ∧ ¬ (𝑥 𝑟𝑟 𝑥)))
217 pm5.17 1035 . . . . . . . . . . . 12 (((𝑥 𝑟𝑟 𝑥) ∧ ¬ (𝑥 𝑟𝑟 𝑥)) ↔ (𝑥 𝑟 ↔ ¬ 𝑟 𝑥))
218216, 217sylib 209 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (𝑥 𝑟 ↔ ¬ 𝑟 𝑥))
219218rexbidva 3196 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (∃𝑥𝐴 𝑥 𝑟 ↔ ∃𝑥𝐴 ¬ 𝑟 𝑥))
22027ad2antrr 717 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝐾 ∈ Toset)
221 simpllr 793 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑟𝐵)
22225sselda 3763 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝐵)
22317, 10trleile 30116 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑦𝐵) → (𝑟 𝑦𝑦 𝑟))
224220, 221, 222, 223syl3anc 1490 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (𝑟 𝑦𝑦 𝑟))
225 simpr 477 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝐴)
226 simplr 785 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ¬ 𝑟𝐴)
227 nelne2 3034 . . . . . . . . . . . . . . . 16 ((𝑦𝐴 ∧ ¬ 𝑟𝐴) → 𝑦𝑟)
228225, 226, 227syl2anc 579 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝑟)
229228necomd 2992 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑟𝑦)
230159adantr 472 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝐾 ∈ Poset)
23117, 10posrasymb 30107 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑦𝐵) → ((𝑟 𝑦𝑦 𝑟) ↔ 𝑟 = 𝑦))
232231necon3bbid 2974 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑦𝐵) → (¬ (𝑟 𝑦𝑦 𝑟) ↔ 𝑟𝑦))
233230, 221, 222, 232syl3anc 1490 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (¬ (𝑟 𝑦𝑦 𝑟) ↔ 𝑟𝑦))
234229, 233mpbird 248 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ¬ (𝑟 𝑦𝑦 𝑟))
235224, 234jca 507 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ((𝑟 𝑦𝑦 𝑟) ∧ ¬ (𝑟 𝑦𝑦 𝑟)))
236 pm5.17 1035 . . . . . . . . . . . 12 (((𝑟 𝑦𝑦 𝑟) ∧ ¬ (𝑟 𝑦𝑦 𝑟)) ↔ (𝑟 𝑦 ↔ ¬ 𝑦 𝑟))
237235, 236sylib 209 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (𝑟 𝑦 ↔ ¬ 𝑦 𝑟))
238237rexbidva 3196 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (∃𝑦𝐴 𝑟 𝑦 ↔ ∃𝑦𝐴 ¬ 𝑦 𝑟))
239219, 238anbi12d 624 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ↔ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)))
240239ex 401 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (¬ 𝑟𝐴 → ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ↔ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟))))
241240pm5.32rd 573 . . . . . . 7 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
242241rexbidva 3196 . . . . . 6 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
243201, 242syl5bb 274 . . . . 5 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
244243biimpa 468 . . . 4 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) → ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴))
2456, 184, 244r19.29af 3223 . . 3 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Conn)
246245ex 401 . 2 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) → ¬ (𝐽t 𝐴) ∈ Conn))
247246con4d 115 1 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → ((𝐽t 𝐴) ∈ Conn → ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wex 1874  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  cdif 3731  cun 3732  cin 3733  wss 3734  c0 4081  {csn 4336   class class class wbr 4811  cmpt 4890   × cxp 5277  dom cdm 5279  ran crn 5280  cfv 6070  (class class class)co 6844  ficfi 8525  Basecbs 16133  lecple 16224  t crest 16350  topGenctg 16367  ordTopcordt 16428   Proset cproset 17195  Posetcpo 17209  Tosetctos 17302  TopOnctopon 20997  Conncconn 21497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-om 7266  df-1st 7368  df-2nd 7369  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-oadd 7770  df-er 7949  df-en 8163  df-fin 8166  df-fi 8526  df-rest 16352  df-topgen 16373  df-ordt 16430  df-proset 17197  df-poset 17215  df-toset 17303  df-top 20981  df-topon 20998  df-bases 21033  df-cld 21106  df-conn 21498
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator