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 33202
Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 33203. See also reconnlem1 24562. (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 1915 . . . . 5 β„²π‘Ÿ(𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡)
2 nfcv 2901 . . . . . . 7 β„²π‘Ÿπ΄
3 nfra2w 3294 . . . . . . 7 β„²π‘Ÿβˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)
42, 3nfralw 3306 . . . . . 6 β„²π‘Ÿβˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)
54nfn 1858 . . . . 5 β„²π‘Ÿ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)
61, 5nfan 1900 . . . 4 β„²π‘Ÿ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
7 tospos 18377 . . . . . . . . . 10 (𝐾 ∈ Toset β†’ 𝐾 ∈ Poset)
8 posprs 18273 . . . . . . . . . 10 (𝐾 ∈ Poset β†’ 𝐾 ∈ Proset )
9 ordtconn.j . . . . . . . . . . 11 𝐽 = (ordTopβ€˜ ≀ )
10 ordtconn.l . . . . . . . . . . . . . 14 ≀ = ((leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡))
11 fvex 6903 . . . . . . . . . . . . . . 15 (leβ€˜πΎ) ∈ V
1211inex1 5316 . . . . . . . . . . . . . 14 ((leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡)) ∈ V
1310, 12eqeltri 2827 . . . . . . . . . . . . 13 ≀ ∈ V
14 eqid 2730 . . . . . . . . . . . . . 14 dom ≀ = dom ≀
1514ordttopon 22917 . . . . . . . . . . . . 13 ( ≀ ∈ V β†’ (ordTopβ€˜ ≀ ) ∈ (TopOnβ€˜dom ≀ ))
1613, 15ax-mp 5 . . . . . . . . . . . 12 (ordTopβ€˜ ≀ ) ∈ (TopOnβ€˜dom ≀ )
17 ordtconn.x . . . . . . . . . . . . . 14 𝐡 = (Baseβ€˜πΎ)
1817, 10prsdm 33192 . . . . . . . . . . . . 13 (𝐾 ∈ Proset β†’ dom ≀ = 𝐡)
1918fveq2d 6894 . . . . . . . . . . . 12 (𝐾 ∈ Proset β†’ (TopOnβ€˜dom ≀ ) = (TopOnβ€˜π΅))
2016, 19eleqtrid 2837 . . . . . . . . . . 11 (𝐾 ∈ Proset β†’ (ordTopβ€˜ ≀ ) ∈ (TopOnβ€˜π΅))
219, 20eqeltrid 2835 . . . . . . . . . 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 5430 . . . . . . . . . . . . . . . 16 {𝐡} ∈ V
3017fvexi 6904 . . . . . . . . . . . . . . . . . . 19 𝐡 ∈ V
3130mptex 7226 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) ∈ V
3231rnex 7905 . . . . . . . . . . . . . . . . 17 ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) ∈ V
3330mptex 7226 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) ∈ V
3433rnex 7905 . . . . . . . . . . . . . . . . 17 ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) ∈ V
3532, 34unex 7735 . . . . . . . . . . . . . . . 16 (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})) ∈ V
3629, 35unex 7735 . . . . . . . . . . . . . . 15 ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) ∈ V
37 ssfii 9416 . . . . . . . . . . . . . . 15 (({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) ∈ V β†’ ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) βŠ† (fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})))))
3836, 37ax-mp 5 . . . . . . . . . . . . . 14 ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) βŠ† (fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))))
39 fvex 6903 . . . . . . . . . . . . . . 15 (fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})))) ∈ V
40 bastg 22689 . . . . . . . . . . . . . . 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 3990 . . . . . . . . . . . . 13 ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) βŠ† (topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})))))
43 eqid 2730 . . . . . . . . . . . . . . 15 ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) = ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
44 eqid 2730 . . . . . . . . . . . . . . 15 ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) = ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
4517, 10, 43, 44ordtprsval 33196 . . . . . . . . . . . . . 14 (𝐾 ∈ Proset β†’ (ordTopβ€˜ ≀ ) = (topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))))))
469, 45eqtrid 2782 . . . . . . . . . . . . 13 (𝐾 ∈ Proset β†’ 𝐽 = (topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))))))
4742, 46sseqtrrid 4034 . . . . . . . . . . . 12 (𝐾 ∈ Proset β†’ ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) βŠ† 𝐽)
4847unssbd 4187 . . . . . . . . . . 11 (𝐾 ∈ Proset β†’ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})) βŠ† 𝐽)
4928, 48syl 17 . . . . . . . . . 10 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})) βŠ† 𝐽)
5049unssbd 4187 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) βŠ† 𝐽)
51 breq2 5151 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 β†’ (π‘Ÿ ≀ 𝑧 ↔ π‘Ÿ ≀ 𝑦))
5251notbid 317 . . . . . . . . . . . . 13 (𝑧 = 𝑦 β†’ (Β¬ π‘Ÿ ≀ 𝑧 ↔ Β¬ π‘Ÿ ≀ 𝑦))
5352cbvrabv 3440 . . . . . . . . . . . 12 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑦}
54 breq1 5150 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ÿ β†’ (π‘₯ ≀ 𝑦 ↔ π‘Ÿ ≀ 𝑦))
5554notbid 317 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ÿ β†’ (Β¬ π‘₯ ≀ 𝑦 ↔ Β¬ π‘Ÿ ≀ 𝑦))
5655rabbidv 3438 . . . . . . . . . . . . 13 (π‘₯ = π‘Ÿ β†’ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑦})
5756rspceeqv 3632 . . . . . . . . . . . 12 ((π‘Ÿ ∈ 𝐡 ∧ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑦}) β†’ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
5853, 57mpan2 687 . . . . . . . . . . 11 (π‘Ÿ ∈ 𝐡 β†’ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
5930rabex 5331 . . . . . . . . . . . 12 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ V
60 eqid 2730 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) = (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
6160elrnmpt 5954 . . . . . . . . . . . 12 ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ V β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) ↔ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))
6259, 61ax-mp 5 . . . . . . . . . . 11 ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) ↔ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
6358, 62sylibr 233 . . . . . . . . . 10 (π‘Ÿ ∈ 𝐡 β†’ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))
6463adantl 480 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))
6550, 64sseldd 3982 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ 𝐽)
6665ad2antrr 722 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ 𝐽)
6749unssad 4186 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βŠ† 𝐽)
68 breq1 5150 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 β†’ (𝑧 ≀ π‘Ÿ ↔ 𝑦 ≀ π‘Ÿ))
6968notbid 317 . . . . . . . . . . . . 13 (𝑧 = 𝑦 β†’ (Β¬ 𝑧 ≀ π‘Ÿ ↔ Β¬ 𝑦 ≀ π‘Ÿ))
7069cbvrabv 3440 . . . . . . . . . . . 12 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘Ÿ}
71 breq2 5151 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ÿ β†’ (𝑦 ≀ π‘₯ ↔ 𝑦 ≀ π‘Ÿ))
7271notbid 317 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ÿ β†’ (Β¬ 𝑦 ≀ π‘₯ ↔ Β¬ 𝑦 ≀ π‘Ÿ))
7372rabbidv 3438 . . . . . . . . . . . . 13 (π‘₯ = π‘Ÿ β†’ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘Ÿ})
7473rspceeqv 3632 . . . . . . . . . . . 12 ((π‘Ÿ ∈ 𝐡 ∧ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘Ÿ}) β†’ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
7570, 74mpan2 687 . . . . . . . . . . 11 (π‘Ÿ ∈ 𝐡 β†’ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
7630rabex 5331 . . . . . . . . . . . 12 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ V
77 eqid 2730 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) = (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
7877elrnmpt 5954 . . . . . . . . . . . 12 ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ V β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) ↔ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}))
7976, 78ax-mp 5 . . . . . . . . . . 11 ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) ↔ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
8075, 79sylibr 233 . . . . . . . . . 10 (π‘Ÿ ∈ 𝐡 β†’ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}))
8180adantl 480 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}))
8267, 81sseldd 3982 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ 𝐽)
8382ad2antrr 722 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ 𝐽)
84 simpll 763 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡))
85 simpr 483 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ Β¬ π‘Ÿ ∈ 𝐴)
8684, 85jca 510 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴))
87 simplrl 773 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯)
88 ssel 3974 . . . . . . . . . . . . . . 15 (𝐴 βŠ† 𝐡 β†’ (π‘₯ ∈ 𝐴 β†’ π‘₯ ∈ 𝐡))
8988ancrd 550 . . . . . . . . . . . . . 14 (𝐴 βŠ† 𝐡 β†’ (π‘₯ ∈ 𝐴 β†’ (π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴)))
9089anim1d 609 . . . . . . . . . . . . 13 (𝐴 βŠ† 𝐡 β†’ ((π‘₯ ∈ 𝐴 ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ ((π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯)))
9190impl 454 . . . . . . . . . . . 12 (((𝐴 βŠ† 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ ((π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯))
92 elin 3963 . . . . . . . . . . . . 13 (π‘₯ ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) ↔ (π‘₯ ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∧ π‘₯ ∈ 𝐴))
93 breq2 5151 . . . . . . . . . . . . . . . 16 (𝑧 = π‘₯ β†’ (π‘Ÿ ≀ 𝑧 ↔ π‘Ÿ ≀ π‘₯))
9493notbid 317 . . . . . . . . . . . . . . 15 (𝑧 = π‘₯ β†’ (Β¬ π‘Ÿ ≀ 𝑧 ↔ Β¬ π‘Ÿ ≀ π‘₯))
9594elrab 3682 . . . . . . . . . . . . . 14 (π‘₯ ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ↔ (π‘₯ ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ π‘₯))
9695anbi1i 622 . . . . . . . . . . . . 13 ((π‘₯ ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∧ π‘₯ ∈ 𝐴) ↔ ((π‘₯ ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ π‘₯) ∧ π‘₯ ∈ 𝐴))
97 an32 642 . . . . . . . . . . . . 13 (((π‘₯ ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ π‘₯) ∧ π‘₯ ∈ 𝐴) ↔ ((π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯))
9892, 96, 973bitri 296 . . . . . . . . . . . 12 (π‘₯ ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) ↔ ((π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯))
9991, 98sylibr 233 . . . . . . . . . . 11 (((𝐴 βŠ† 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ π‘₯ ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴))
10099ne0d 4334 . . . . . . . . . 10 (((𝐴 βŠ† 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) β‰  βˆ…)
10125, 100sylanl1 676 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) β‰  βˆ…)
102101r19.29an 3156 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) β‰  βˆ…)
10386, 87, 102syl2anc 582 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) β‰  βˆ…)
104 simplrr 774 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)
105 ssel 3974 . . . . . . . . . . . . . . 15 (𝐴 βŠ† 𝐡 β†’ (𝑦 ∈ 𝐴 β†’ 𝑦 ∈ 𝐡))
106105ancrd 550 . . . . . . . . . . . . . 14 (𝐴 βŠ† 𝐡 β†’ (𝑦 ∈ 𝐴 β†’ (𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴)))
107106anim1d 609 . . . . . . . . . . . . 13 (𝐴 βŠ† 𝐡 β†’ ((𝑦 ∈ 𝐴 ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ ((𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ)))
108107impl 454 . . . . . . . . . . . 12 (((𝐴 βŠ† 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ ((𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ))
109 elin 3963 . . . . . . . . . . . . 13 (𝑦 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) ↔ (𝑦 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∧ 𝑦 ∈ 𝐴))
11069elrab 3682 . . . . . . . . . . . . . 14 (𝑦 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ↔ (𝑦 ∈ 𝐡 ∧ Β¬ 𝑦 ≀ π‘Ÿ))
111110anbi1i 622 . . . . . . . . . . . . 13 ((𝑦 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐡 ∧ Β¬ 𝑦 ≀ π‘Ÿ) ∧ 𝑦 ∈ 𝐴))
112 an32 642 . . . . . . . . . . . . 13 (((𝑦 ∈ 𝐡 ∧ Β¬ 𝑦 ≀ π‘Ÿ) ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ))
113109, 111, 1123bitri 296 . . . . . . . . . . . 12 (𝑦 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) ↔ ((𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ))
114108, 113sylibr 233 . . . . . . . . . . 11 (((𝐴 βŠ† 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ 𝑦 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴))
115114ne0d 4334 . . . . . . . . . 10 (((𝐴 βŠ† 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) β‰  βˆ…)
11625, 115sylanl1 676 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) β‰  βˆ…)
117116r19.29an 3156 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) β‰  βˆ…)
11886, 104, 117syl2anc 582 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) β‰  βˆ…)
11917, 10trleile 32408 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (π‘Ÿ ≀ 𝑧 ∨ 𝑧 ≀ π‘Ÿ))
120 oran 986 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ≀ 𝑧 ∨ 𝑧 ≀ π‘Ÿ) ↔ Β¬ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
121119, 120sylib 217 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ Β¬ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
1221213expa 1116 . . . . . . . . . . . . . 14 (((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ Β¬ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
123122nrexdv 3147 . . . . . . . . . . . . 13 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡) β†’ Β¬ βˆƒπ‘§ ∈ 𝐡 (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
124 rabid 3450 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ↔ (𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧))
125 rabid 3450 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ↔ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
126124, 125anbi12i 625 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ ((𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧) ∧ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
127 elin 3963 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
128 anandi 672 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ)) ↔ ((𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧) ∧ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
129126, 127, 1283bitr4i 302 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ (𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
130129exbii 1848 . . . . . . . . . . . . . . 15 (βˆƒπ‘§ 𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ βˆƒπ‘§(𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
131 nfrab1 3449 . . . . . . . . . . . . . . . . 17 Ⅎ𝑧{𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧}
132 nfrab1 3449 . . . . . . . . . . . . . . . . 17 Ⅎ𝑧{𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}
133131, 132nfin 4215 . . . . . . . . . . . . . . . 16 Ⅎ𝑧({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ})
134133n0f 4341 . . . . . . . . . . . . . . 15 (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) β‰  βˆ… ↔ βˆƒπ‘§ 𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
135 df-rex 3069 . . . . . . . . . . . . . . 15 (βˆƒπ‘§ ∈ 𝐡 (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ) ↔ βˆƒπ‘§(𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
136130, 134, 1353bitr4i 302 . . . . . . . . . . . . . 14 (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) β‰  βˆ… ↔ βˆƒπ‘§ ∈ 𝐡 (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
137136necon1bbii 2988 . . . . . . . . . . . . 13 (Β¬ βˆƒπ‘§ ∈ 𝐡 (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ) ↔ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = βˆ…)
138123, 137sylib 217 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = βˆ…)
139138adantlr 711 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = βˆ…)
140139adantr 479 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = βˆ…)
141140ineq1d 4210 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ∩ 𝐴) = (βˆ… ∩ 𝐴))
142 0in 4392 . . . . . . . . 9 (βˆ… ∩ 𝐴) = βˆ…
143141, 142eqtrdi 2786 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ∩ 𝐴) = βˆ…)
144143adantlr 711 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ∩ 𝐴) = βˆ…)
145 simplr 765 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ π‘Ÿ ∈ 𝐡)
146 simpr 483 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ Β¬ π‘Ÿ ∈ 𝐴)
147 vex 3476 . . . . . . . . . . . . . . 15 π‘Ÿ ∈ V
148147snss 4788 . . . . . . . . . . . . . 14 (π‘Ÿ ∈ 𝐡 ↔ {π‘Ÿ} βŠ† 𝐡)
149 eldif 3957 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ (𝐡 βˆ– 𝐴) ↔ (π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴))
150147snss 4788 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ (𝐡 βˆ– 𝐴) ↔ {π‘Ÿ} βŠ† (𝐡 βˆ– 𝐴))
151149, 150bitr3i 276 . . . . . . . . . . . . . . 15 ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ {π‘Ÿ} βŠ† (𝐡 βˆ– 𝐴))
152 ssconb 4136 . . . . . . . . . . . . . . 15 (({π‘Ÿ} βŠ† 𝐡 ∧ 𝐴 βŠ† 𝐡) β†’ ({π‘Ÿ} βŠ† (𝐡 βˆ– 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
153151, 152bitrid 282 . . . . . . . . . . . . . 14 (({π‘Ÿ} βŠ† 𝐡 ∧ 𝐴 βŠ† 𝐡) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
154148, 153sylanb 579 . . . . . . . . . . . . 13 ((π‘Ÿ ∈ 𝐡 ∧ 𝐴 βŠ† 𝐡) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
155154adantl 480 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ (π‘Ÿ ∈ 𝐡 ∧ 𝐴 βŠ† 𝐡)) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
156155anass1rs 651 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
157156adantr 479 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
158145, 146, 157mpbi2and 708 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ}))
1597ad3antrrr 726 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐾 ∈ Poset)
160 nfv 1915 . . . . . . . . . . 11 Ⅎ𝑧(𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡)
161131, 132nfun 4164 . . . . . . . . . . 11 Ⅎ𝑧({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ})
162 nfcv 2901 . . . . . . . . . . 11 Ⅎ𝑧(𝐡 βˆ– {π‘Ÿ})
163 ianor 978 . . . . . . . . . . . . . . 15 (Β¬ (π‘Ÿ ≀ 𝑧 ∧ 𝑧 ≀ π‘Ÿ) ↔ (Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ))
16417, 10posrasymb 32402 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ ((π‘Ÿ ≀ 𝑧 ∧ 𝑧 ≀ π‘Ÿ) ↔ π‘Ÿ = 𝑧))
165 equcom 2019 . . . . . . . . . . . . . . . . 17 (π‘Ÿ = 𝑧 ↔ 𝑧 = π‘Ÿ)
166164, 165bitrdi 286 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ ((π‘Ÿ ≀ 𝑧 ∧ 𝑧 ≀ π‘Ÿ) ↔ 𝑧 = π‘Ÿ))
167166necon3bbid 2976 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (Β¬ (π‘Ÿ ≀ 𝑧 ∧ 𝑧 ≀ π‘Ÿ) ↔ 𝑧 β‰  π‘Ÿ))
168163, 167bitr3id 284 . . . . . . . . . . . . . 14 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ ((Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ) ↔ 𝑧 β‰  π‘Ÿ))
1691683expia 1119 . . . . . . . . . . . . 13 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡) β†’ (𝑧 ∈ 𝐡 β†’ ((Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ) ↔ 𝑧 β‰  π‘Ÿ)))
170169pm5.32d 575 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡) β†’ ((𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ)) ↔ (𝑧 ∈ 𝐡 ∧ 𝑧 β‰  π‘Ÿ)))
171124, 125orbi12i 911 . . . . . . . . . . . . 13 ((𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ ((𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧) ∨ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
172 elun 4147 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
173 andi 1004 . . . . . . . . . . . . 13 ((𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ)) ↔ ((𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧) ∨ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
174171, 172, 1733bitr4ri 303 . . . . . . . . . . . 12 ((𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ)) ↔ 𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
175 eldifsn 4789 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐡 βˆ– {π‘Ÿ}) ↔ (𝑧 ∈ 𝐡 ∧ 𝑧 β‰  π‘Ÿ))
176175bicomi 223 . . . . . . . . . . . 12 ((𝑧 ∈ 𝐡 ∧ 𝑧 β‰  π‘Ÿ) ↔ 𝑧 ∈ (𝐡 βˆ– {π‘Ÿ}))
177170, 174, 1763bitr3g 312 . . . . . . . . . . 11 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡) β†’ (𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ 𝑧 ∈ (𝐡 βˆ– {π‘Ÿ})))
178160, 161, 162, 177eqrd 4000 . . . . . . . . . 10 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = (𝐡 βˆ– {π‘Ÿ}))
179159, 145, 178syl2anc 582 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = (𝐡 βˆ– {π‘Ÿ}))
180158, 179sseqtrrd 4022 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐴 βŠ† ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
181180adantlr 711 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐴 βŠ† ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
18224, 26, 66, 83, 103, 118, 144, 181nconnsubb 23147 . . . . . 6 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ Β¬ (𝐽 β†Ύt 𝐴) ∈ Conn)
183182anasss 465 . . . . 5 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)) β†’ Β¬ (𝐽 β†Ύt 𝐴) ∈ Conn)
184183adantllr 715 . . . 4 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)) ∧ π‘Ÿ ∈ 𝐡) ∧ ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)) β†’ Β¬ (𝐽 β†Ύt 𝐴) ∈ Conn)
185 rexanali 3100 . . . . . . . . . . 11 (βˆƒπ‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
186185rexbii 3092 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘¦ ∈ 𝐴 Β¬ βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
187 rexcom 3285 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
188 rexnal 3098 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ 𝐴 Β¬ βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
189186, 187, 1883bitr3i 300 . . . . . . . . 9 (βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
190189rexbii 3092 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘₯ ∈ 𝐴 Β¬ βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
191 rexcom 3285 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
192 rexnal 3098 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐴 Β¬ βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
193190, 191, 1923bitr3i 300 . . . . . . 7 (βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
194 r19.41v 3186 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ (βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
195194rexbii 3092 . . . . . . . . 9 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘₯ ∈ 𝐴 (βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
196 r19.41v 3186 . . . . . . . . 9 (βˆƒπ‘₯ ∈ 𝐴 (βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
197 reeanv 3224 . . . . . . . . . 10 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ↔ (βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦))
198197anbi1i 622 . . . . . . . . 9 ((βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
199195, 196, 1983bitri 296 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
200199rexbii 3092 . . . . . . 7 (βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
201193, 200bitr3i 276 . . . . . 6 (Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
20227ad2antrr 722 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ 𝐾 ∈ Toset)
20325sselda 3981 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ 𝐡)
204 simpllr 772 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ π‘Ÿ ∈ 𝐡)
20517, 10trleile 32408 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) β†’ (π‘₯ ≀ π‘Ÿ ∨ π‘Ÿ ≀ π‘₯))
206202, 203, 204, 205syl3anc 1369 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ (π‘₯ ≀ π‘Ÿ ∨ π‘Ÿ ≀ π‘₯))
207 simpr 483 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ 𝐴)
208 simplr 765 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ Β¬ π‘Ÿ ∈ 𝐴)
209 nelne2 3038 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ 𝐴 ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ π‘₯ β‰  π‘Ÿ)
210207, 208, 209syl2anc 582 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ β‰  π‘Ÿ)
211159adantr 479 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ 𝐾 ∈ Poset)
21217, 10posrasymb 32402 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) β†’ ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯) ↔ π‘₯ = π‘Ÿ))
213212necon3bbid 2976 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) β†’ (Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯) ↔ π‘₯ β‰  π‘Ÿ))
214211, 203, 204, 213syl3anc 1369 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ (Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯) ↔ π‘₯ β‰  π‘Ÿ))
215210, 214mpbird 256 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯))
216206, 215jca 510 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ ((π‘₯ ≀ π‘Ÿ ∨ π‘Ÿ ≀ π‘₯) ∧ Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯)))
217 pm5.17 1008 . . . . . . . . . . . 12 (((π‘₯ ≀ π‘Ÿ ∨ π‘Ÿ ≀ π‘₯) ∧ Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯)) ↔ (π‘₯ ≀ π‘Ÿ ↔ Β¬ π‘Ÿ ≀ π‘₯))
218216, 217sylib 217 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ (π‘₯ ≀ π‘Ÿ ↔ Β¬ π‘Ÿ ≀ π‘₯))
219218rexbidva 3174 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ↔ βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯))
22027ad2antrr 722 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝐾 ∈ Toset)
221 simpllr 772 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ π‘Ÿ ∈ 𝐡)
22225sselda 3981 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝑦 ∈ 𝐡)
22317, 10trleile 32408 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ (π‘Ÿ ≀ 𝑦 ∨ 𝑦 ≀ π‘Ÿ))
224220, 221, 222, 223syl3anc 1369 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ (π‘Ÿ ≀ 𝑦 ∨ 𝑦 ≀ π‘Ÿ))
225 simpr 483 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝑦 ∈ 𝐴)
226 simplr 765 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ Β¬ π‘Ÿ ∈ 𝐴)
227 nelne2 3038 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ 𝐴 ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝑦 β‰  π‘Ÿ)
228225, 226, 227syl2anc 582 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝑦 β‰  π‘Ÿ)
229228necomd 2994 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ π‘Ÿ β‰  𝑦)
230159adantr 479 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝐾 ∈ Poset)
23117, 10posrasymb 32402 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ ((π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ) ↔ π‘Ÿ = 𝑦))
232231necon3bbid 2976 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ (Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ) ↔ π‘Ÿ β‰  𝑦))
233230, 221, 222, 232syl3anc 1369 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ (Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ) ↔ π‘Ÿ β‰  𝑦))
234229, 233mpbird 256 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ))
235224, 234jca 510 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ ((π‘Ÿ ≀ 𝑦 ∨ 𝑦 ≀ π‘Ÿ) ∧ Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ)))
236 pm5.17 1008 . . . . . . . . . . . 12 (((π‘Ÿ ≀ 𝑦 ∨ 𝑦 ≀ π‘Ÿ) ∧ Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ)) ↔ (π‘Ÿ ≀ 𝑦 ↔ Β¬ 𝑦 ≀ π‘Ÿ))
237235, 236sylib 217 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ (π‘Ÿ ≀ 𝑦 ↔ Β¬ 𝑦 ≀ π‘Ÿ))
238237rexbidva 3174 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦 ↔ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ))
239219, 238anbi12d 629 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ↔ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)))
240239ex 411 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ (Β¬ π‘Ÿ ∈ 𝐴 β†’ ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ↔ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ))))
241240pm5.32rd 576 . . . . . . 7 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ (((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)))
242241rexbidva 3174 . . . . . 6 ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) β†’ (βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)))
243201, 242bitrid 282 . . . . 5 ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) β†’ (Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)))
244243biimpa 475 . . . 4 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)) β†’ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴))
2456, 184, 244r19.29af 3263 . . 3 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)) β†’ Β¬ (𝐽 β†Ύt 𝐴) ∈ Conn)
246245ex 411 . 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 394   ∨ wo 843   ∧ w3a 1085   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  {crab 3430  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  {csn 4627   class class class wbr 5147   ↦ cmpt 5230   Γ— cxp 5673  dom cdm 5675  ran crn 5676  β€˜cfv 6542  (class class class)co 7411  ficfi 9407  Basecbs 17148  lecple 17208   β†Ύt crest 17370  topGenctg 17387  ordTopcordt 17449   Proset cproset 18250  Posetcpo 18264  Tosetctos 18373  TopOnctopon 22632  Conncconn 23135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-1o 8468  df-er 8705  df-en 8942  df-fin 8945  df-fi 9408  df-rest 17372  df-topgen 17393  df-ordt 17451  df-proset 18252  df-poset 18270  df-toset 18374  df-top 22616  df-topon 22633  df-bases 22669  df-cld 22743  df-conn 23136
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator