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 32893
Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 32894. See also reconnlem1 24334. (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 1918 . . . . 5 β„²π‘Ÿ(𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡)
2 nfcv 2904 . . . . . . 7 β„²π‘Ÿπ΄
3 nfra2w 3297 . . . . . . 7 β„²π‘Ÿβˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)
42, 3nfralw 3309 . . . . . 6 β„²π‘Ÿβˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)
54nfn 1861 . . . . 5 β„²π‘Ÿ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)
61, 5nfan 1903 . . . 4 β„²π‘Ÿ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
7 tospos 18370 . . . . . . . . . 10 (𝐾 ∈ Toset β†’ 𝐾 ∈ Poset)
8 posprs 18266 . . . . . . . . . 10 (𝐾 ∈ Poset β†’ 𝐾 ∈ Proset )
9 ordtconn.j . . . . . . . . . . 11 𝐽 = (ordTopβ€˜ ≀ )
10 ordtconn.l . . . . . . . . . . . . . 14 ≀ = ((leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡))
11 fvex 6902 . . . . . . . . . . . . . . 15 (leβ€˜πΎ) ∈ V
1211inex1 5317 . . . . . . . . . . . . . 14 ((leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡)) ∈ V
1310, 12eqeltri 2830 . . . . . . . . . . . . 13 ≀ ∈ V
14 eqid 2733 . . . . . . . . . . . . . 14 dom ≀ = dom ≀
1514ordttopon 22689 . . . . . . . . . . . . 13 ( ≀ ∈ V β†’ (ordTopβ€˜ ≀ ) ∈ (TopOnβ€˜dom ≀ ))
1613, 15ax-mp 5 . . . . . . . . . . . 12 (ordTopβ€˜ ≀ ) ∈ (TopOnβ€˜dom ≀ )
17 ordtconn.x . . . . . . . . . . . . . 14 𝐡 = (Baseβ€˜πΎ)
1817, 10prsdm 32883 . . . . . . . . . . . . 13 (𝐾 ∈ Proset β†’ dom ≀ = 𝐡)
1918fveq2d 6893 . . . . . . . . . . . 12 (𝐾 ∈ Proset β†’ (TopOnβ€˜dom ≀ ) = (TopOnβ€˜π΅))
2016, 19eleqtrid 2840 . . . . . . . . . . 11 (𝐾 ∈ Proset β†’ (ordTopβ€˜ ≀ ) ∈ (TopOnβ€˜π΅))
219, 20eqeltrid 2838 . . . . . . . . . 10 (𝐾 ∈ Proset β†’ 𝐽 ∈ (TopOnβ€˜π΅))
227, 8, 213syl 18 . . . . . . . . 9 (𝐾 ∈ Toset β†’ 𝐽 ∈ (TopOnβ€˜π΅))
2322ad3antrrr 729 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐽 ∈ (TopOnβ€˜π΅))
2423adantlr 714 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐽 ∈ (TopOnβ€˜π΅))
25 simpllr 775 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐴 βŠ† 𝐡)
2625adantlr 714 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐴 βŠ† 𝐡)
27 simpll 766 . . . . . . . . . . . 12 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ 𝐾 ∈ Toset)
2827, 7, 83syl 18 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ 𝐾 ∈ Proset )
29 snex 5431 . . . . . . . . . . . . . . . 16 {𝐡} ∈ V
3017fvexi 6903 . . . . . . . . . . . . . . . . . . 19 𝐡 ∈ V
3130mptex 7222 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) ∈ V
3231rnex 7900 . . . . . . . . . . . . . . . . 17 ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) ∈ V
3330mptex 7222 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) ∈ V
3433rnex 7900 . . . . . . . . . . . . . . . . 17 ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) ∈ V
3532, 34unex 7730 . . . . . . . . . . . . . . . 16 (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})) ∈ V
3629, 35unex 7730 . . . . . . . . . . . . . . 15 ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) ∈ V
37 ssfii 9411 . . . . . . . . . . . . . . 15 (({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) ∈ V β†’ ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) βŠ† (fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})))))
3836, 37ax-mp 5 . . . . . . . . . . . . . 14 ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) βŠ† (fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))))
39 fvex 6902 . . . . . . . . . . . . . . 15 (fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})))) ∈ V
40 bastg 22461 . . . . . . . . . . . . . . 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 3991 . . . . . . . . . . . . 13 ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) βŠ† (topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})))))
43 eqid 2733 . . . . . . . . . . . . . . 15 ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) = ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
44 eqid 2733 . . . . . . . . . . . . . . 15 ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) = ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
4517, 10, 43, 44ordtprsval 32887 . . . . . . . . . . . . . 14 (𝐾 ∈ Proset β†’ (ordTopβ€˜ ≀ ) = (topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))))))
469, 45eqtrid 2785 . . . . . . . . . . . . 13 (𝐾 ∈ Proset β†’ 𝐽 = (topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))))))
4742, 46sseqtrrid 4035 . . . . . . . . . . . 12 (𝐾 ∈ Proset β†’ ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) βŠ† 𝐽)
4847unssbd 4188 . . . . . . . . . . 11 (𝐾 ∈ Proset β†’ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})) βŠ† 𝐽)
4928, 48syl 17 . . . . . . . . . 10 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})) βŠ† 𝐽)
5049unssbd 4188 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) βŠ† 𝐽)
51 breq2 5152 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 β†’ (π‘Ÿ ≀ 𝑧 ↔ π‘Ÿ ≀ 𝑦))
5251notbid 318 . . . . . . . . . . . . 13 (𝑧 = 𝑦 β†’ (Β¬ π‘Ÿ ≀ 𝑧 ↔ Β¬ π‘Ÿ ≀ 𝑦))
5352cbvrabv 3443 . . . . . . . . . . . 12 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑦}
54 breq1 5151 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ÿ β†’ (π‘₯ ≀ 𝑦 ↔ π‘Ÿ ≀ 𝑦))
5554notbid 318 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ÿ β†’ (Β¬ π‘₯ ≀ 𝑦 ↔ Β¬ π‘Ÿ ≀ 𝑦))
5655rabbidv 3441 . . . . . . . . . . . . 13 (π‘₯ = π‘Ÿ β†’ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑦})
5756rspceeqv 3633 . . . . . . . . . . . 12 ((π‘Ÿ ∈ 𝐡 ∧ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑦}) β†’ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
5853, 57mpan2 690 . . . . . . . . . . 11 (π‘Ÿ ∈ 𝐡 β†’ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
5930rabex 5332 . . . . . . . . . . . 12 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ V
60 eqid 2733 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) = (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
6160elrnmpt 5954 . . . . . . . . . . . 12 ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ V β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) ↔ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))
6259, 61ax-mp 5 . . . . . . . . . . 11 ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) ↔ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
6358, 62sylibr 233 . . . . . . . . . 10 (π‘Ÿ ∈ 𝐡 β†’ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))
6463adantl 483 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))
6550, 64sseldd 3983 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ 𝐽)
6665ad2antrr 725 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ 𝐽)
6749unssad 4187 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βŠ† 𝐽)
68 breq1 5151 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 β†’ (𝑧 ≀ π‘Ÿ ↔ 𝑦 ≀ π‘Ÿ))
6968notbid 318 . . . . . . . . . . . . 13 (𝑧 = 𝑦 β†’ (Β¬ 𝑧 ≀ π‘Ÿ ↔ Β¬ 𝑦 ≀ π‘Ÿ))
7069cbvrabv 3443 . . . . . . . . . . . 12 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘Ÿ}
71 breq2 5152 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ÿ β†’ (𝑦 ≀ π‘₯ ↔ 𝑦 ≀ π‘Ÿ))
7271notbid 318 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ÿ β†’ (Β¬ 𝑦 ≀ π‘₯ ↔ Β¬ 𝑦 ≀ π‘Ÿ))
7372rabbidv 3441 . . . . . . . . . . . . 13 (π‘₯ = π‘Ÿ β†’ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘Ÿ})
7473rspceeqv 3633 . . . . . . . . . . . 12 ((π‘Ÿ ∈ 𝐡 ∧ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘Ÿ}) β†’ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
7570, 74mpan2 690 . . . . . . . . . . 11 (π‘Ÿ ∈ 𝐡 β†’ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
7630rabex 5332 . . . . . . . . . . . 12 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ V
77 eqid 2733 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) = (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
7877elrnmpt 5954 . . . . . . . . . . . 12 ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ V β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) ↔ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}))
7976, 78ax-mp 5 . . . . . . . . . . 11 ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) ↔ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
8075, 79sylibr 233 . . . . . . . . . 10 (π‘Ÿ ∈ 𝐡 β†’ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}))
8180adantl 483 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}))
8267, 81sseldd 3983 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ 𝐽)
8382ad2antrr 725 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ 𝐽)
84 simpll 766 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡))
85 simpr 486 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ Β¬ π‘Ÿ ∈ 𝐴)
8684, 85jca 513 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴))
87 simplrl 776 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯)
88 ssel 3975 . . . . . . . . . . . . . . 15 (𝐴 βŠ† 𝐡 β†’ (π‘₯ ∈ 𝐴 β†’ π‘₯ ∈ 𝐡))
8988ancrd 553 . . . . . . . . . . . . . 14 (𝐴 βŠ† 𝐡 β†’ (π‘₯ ∈ 𝐴 β†’ (π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴)))
9089anim1d 612 . . . . . . . . . . . . 13 (𝐴 βŠ† 𝐡 β†’ ((π‘₯ ∈ 𝐴 ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ ((π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯)))
9190impl 457 . . . . . . . . . . . 12 (((𝐴 βŠ† 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ ((π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯))
92 elin 3964 . . . . . . . . . . . . 13 (π‘₯ ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) ↔ (π‘₯ ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∧ π‘₯ ∈ 𝐴))
93 breq2 5152 . . . . . . . . . . . . . . . 16 (𝑧 = π‘₯ β†’ (π‘Ÿ ≀ 𝑧 ↔ π‘Ÿ ≀ π‘₯))
9493notbid 318 . . . . . . . . . . . . . . 15 (𝑧 = π‘₯ β†’ (Β¬ π‘Ÿ ≀ 𝑧 ↔ Β¬ π‘Ÿ ≀ π‘₯))
9594elrab 3683 . . . . . . . . . . . . . 14 (π‘₯ ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ↔ (π‘₯ ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ π‘₯))
9695anbi1i 625 . . . . . . . . . . . . 13 ((π‘₯ ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∧ π‘₯ ∈ 𝐴) ↔ ((π‘₯ ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ π‘₯) ∧ π‘₯ ∈ 𝐴))
97 an32 645 . . . . . . . . . . . . 13 (((π‘₯ ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ π‘₯) ∧ π‘₯ ∈ 𝐴) ↔ ((π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯))
9892, 96, 973bitri 297 . . . . . . . . . . . 12 (π‘₯ ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) ↔ ((π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯))
9991, 98sylibr 233 . . . . . . . . . . 11 (((𝐴 βŠ† 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ π‘₯ ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴))
10099ne0d 4335 . . . . . . . . . 10 (((𝐴 βŠ† 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) β‰  βˆ…)
10125, 100sylanl1 679 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) β‰  βˆ…)
102101r19.29an 3159 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) β‰  βˆ…)
10386, 87, 102syl2anc 585 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) β‰  βˆ…)
104 simplrr 777 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)
105 ssel 3975 . . . . . . . . . . . . . . 15 (𝐴 βŠ† 𝐡 β†’ (𝑦 ∈ 𝐴 β†’ 𝑦 ∈ 𝐡))
106105ancrd 553 . . . . . . . . . . . . . 14 (𝐴 βŠ† 𝐡 β†’ (𝑦 ∈ 𝐴 β†’ (𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴)))
107106anim1d 612 . . . . . . . . . . . . 13 (𝐴 βŠ† 𝐡 β†’ ((𝑦 ∈ 𝐴 ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ ((𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ)))
108107impl 457 . . . . . . . . . . . 12 (((𝐴 βŠ† 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ ((𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ))
109 elin 3964 . . . . . . . . . . . . 13 (𝑦 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) ↔ (𝑦 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∧ 𝑦 ∈ 𝐴))
11069elrab 3683 . . . . . . . . . . . . . 14 (𝑦 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ↔ (𝑦 ∈ 𝐡 ∧ Β¬ 𝑦 ≀ π‘Ÿ))
111110anbi1i 625 . . . . . . . . . . . . 13 ((𝑦 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐡 ∧ Β¬ 𝑦 ≀ π‘Ÿ) ∧ 𝑦 ∈ 𝐴))
112 an32 645 . . . . . . . . . . . . 13 (((𝑦 ∈ 𝐡 ∧ Β¬ 𝑦 ≀ π‘Ÿ) ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ))
113109, 111, 1123bitri 297 . . . . . . . . . . . 12 (𝑦 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) ↔ ((𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ))
114108, 113sylibr 233 . . . . . . . . . . 11 (((𝐴 βŠ† 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ 𝑦 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴))
115114ne0d 4335 . . . . . . . . . 10 (((𝐴 βŠ† 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) β‰  βˆ…)
11625, 115sylanl1 679 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) β‰  βˆ…)
117116r19.29an 3159 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) β‰  βˆ…)
11886, 104, 117syl2anc 585 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) β‰  βˆ…)
11917, 10trleile 32129 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (π‘Ÿ ≀ 𝑧 ∨ 𝑧 ≀ π‘Ÿ))
120 oran 989 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ≀ 𝑧 ∨ 𝑧 ≀ π‘Ÿ) ↔ Β¬ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
121119, 120sylib 217 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ Β¬ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
1221213expa 1119 . . . . . . . . . . . . . 14 (((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ Β¬ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
123122nrexdv 3150 . . . . . . . . . . . . 13 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡) β†’ Β¬ βˆƒπ‘§ ∈ 𝐡 (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
124 rabid 3453 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ↔ (𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧))
125 rabid 3453 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ↔ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
126124, 125anbi12i 628 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ ((𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧) ∧ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
127 elin 3964 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
128 anandi 675 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ)) ↔ ((𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧) ∧ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
129126, 127, 1283bitr4i 303 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ (𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
130129exbii 1851 . . . . . . . . . . . . . . 15 (βˆƒπ‘§ 𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ βˆƒπ‘§(𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
131 nfrab1 3452 . . . . . . . . . . . . . . . . 17 Ⅎ𝑧{𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧}
132 nfrab1 3452 . . . . . . . . . . . . . . . . 17 Ⅎ𝑧{𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}
133131, 132nfin 4216 . . . . . . . . . . . . . . . 16 Ⅎ𝑧({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ})
134133n0f 4342 . . . . . . . . . . . . . . 15 (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) β‰  βˆ… ↔ βˆƒπ‘§ 𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
135 df-rex 3072 . . . . . . . . . . . . . . 15 (βˆƒπ‘§ ∈ 𝐡 (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ) ↔ βˆƒπ‘§(𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
136130, 134, 1353bitr4i 303 . . . . . . . . . . . . . 14 (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) β‰  βˆ… ↔ βˆƒπ‘§ ∈ 𝐡 (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
137136necon1bbii 2991 . . . . . . . . . . . . 13 (Β¬ βˆƒπ‘§ ∈ 𝐡 (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ) ↔ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = βˆ…)
138123, 137sylib 217 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = βˆ…)
139138adantlr 714 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = βˆ…)
140139adantr 482 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = βˆ…)
141140ineq1d 4211 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ∩ 𝐴) = (βˆ… ∩ 𝐴))
142 0in 4393 . . . . . . . . 9 (βˆ… ∩ 𝐴) = βˆ…
143141, 142eqtrdi 2789 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ∩ 𝐴) = βˆ…)
144143adantlr 714 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ∩ 𝐴) = βˆ…)
145 simplr 768 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ π‘Ÿ ∈ 𝐡)
146 simpr 486 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ Β¬ π‘Ÿ ∈ 𝐴)
147 vex 3479 . . . . . . . . . . . . . . 15 π‘Ÿ ∈ V
148147snss 4789 . . . . . . . . . . . . . 14 (π‘Ÿ ∈ 𝐡 ↔ {π‘Ÿ} βŠ† 𝐡)
149 eldif 3958 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ (𝐡 βˆ– 𝐴) ↔ (π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴))
150147snss 4789 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ (𝐡 βˆ– 𝐴) ↔ {π‘Ÿ} βŠ† (𝐡 βˆ– 𝐴))
151149, 150bitr3i 277 . . . . . . . . . . . . . . 15 ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ {π‘Ÿ} βŠ† (𝐡 βˆ– 𝐴))
152 ssconb 4137 . . . . . . . . . . . . . . 15 (({π‘Ÿ} βŠ† 𝐡 ∧ 𝐴 βŠ† 𝐡) β†’ ({π‘Ÿ} βŠ† (𝐡 βˆ– 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
153151, 152bitrid 283 . . . . . . . . . . . . . 14 (({π‘Ÿ} βŠ† 𝐡 ∧ 𝐴 βŠ† 𝐡) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
154148, 153sylanb 582 . . . . . . . . . . . . 13 ((π‘Ÿ ∈ 𝐡 ∧ 𝐴 βŠ† 𝐡) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
155154adantl 483 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ (π‘Ÿ ∈ 𝐡 ∧ 𝐴 βŠ† 𝐡)) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
156155anass1rs 654 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
157156adantr 482 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
158145, 146, 157mpbi2and 711 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ}))
1597ad3antrrr 729 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐾 ∈ Poset)
160 nfv 1918 . . . . . . . . . . 11 Ⅎ𝑧(𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡)
161131, 132nfun 4165 . . . . . . . . . . 11 Ⅎ𝑧({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ})
162 nfcv 2904 . . . . . . . . . . 11 Ⅎ𝑧(𝐡 βˆ– {π‘Ÿ})
163 ianor 981 . . . . . . . . . . . . . . 15 (Β¬ (π‘Ÿ ≀ 𝑧 ∧ 𝑧 ≀ π‘Ÿ) ↔ (Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ))
16417, 10posrasymb 32123 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ ((π‘Ÿ ≀ 𝑧 ∧ 𝑧 ≀ π‘Ÿ) ↔ π‘Ÿ = 𝑧))
165 equcom 2022 . . . . . . . . . . . . . . . . 17 (π‘Ÿ = 𝑧 ↔ 𝑧 = π‘Ÿ)
166164, 165bitrdi 287 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ ((π‘Ÿ ≀ 𝑧 ∧ 𝑧 ≀ π‘Ÿ) ↔ 𝑧 = π‘Ÿ))
167166necon3bbid 2979 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (Β¬ (π‘Ÿ ≀ 𝑧 ∧ 𝑧 ≀ π‘Ÿ) ↔ 𝑧 β‰  π‘Ÿ))
168163, 167bitr3id 285 . . . . . . . . . . . . . 14 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ ((Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ) ↔ 𝑧 β‰  π‘Ÿ))
1691683expia 1122 . . . . . . . . . . . . 13 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡) β†’ (𝑧 ∈ 𝐡 β†’ ((Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ) ↔ 𝑧 β‰  π‘Ÿ)))
170169pm5.32d 578 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡) β†’ ((𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ)) ↔ (𝑧 ∈ 𝐡 ∧ 𝑧 β‰  π‘Ÿ)))
171124, 125orbi12i 914 . . . . . . . . . . . . 13 ((𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ ((𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧) ∨ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
172 elun 4148 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
173 andi 1007 . . . . . . . . . . . . 13 ((𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ)) ↔ ((𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧) ∨ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
174171, 172, 1733bitr4ri 304 . . . . . . . . . . . 12 ((𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ)) ↔ 𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
175 eldifsn 4790 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐡 βˆ– {π‘Ÿ}) ↔ (𝑧 ∈ 𝐡 ∧ 𝑧 β‰  π‘Ÿ))
176175bicomi 223 . . . . . . . . . . . 12 ((𝑧 ∈ 𝐡 ∧ 𝑧 β‰  π‘Ÿ) ↔ 𝑧 ∈ (𝐡 βˆ– {π‘Ÿ}))
177170, 174, 1763bitr3g 313 . . . . . . . . . . 11 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡) β†’ (𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ 𝑧 ∈ (𝐡 βˆ– {π‘Ÿ})))
178160, 161, 162, 177eqrd 4001 . . . . . . . . . 10 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = (𝐡 βˆ– {π‘Ÿ}))
179159, 145, 178syl2anc 585 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = (𝐡 βˆ– {π‘Ÿ}))
180158, 179sseqtrrd 4023 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐴 βŠ† ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
181180adantlr 714 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐴 βŠ† ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
18224, 26, 66, 83, 103, 118, 144, 181nconnsubb 22919 . . . . . 6 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ Β¬ (𝐽 β†Ύt 𝐴) ∈ Conn)
183182anasss 468 . . . . 5 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)) β†’ Β¬ (𝐽 β†Ύt 𝐴) ∈ Conn)
184183adantllr 718 . . . 4 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)) ∧ π‘Ÿ ∈ 𝐡) ∧ ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)) β†’ Β¬ (𝐽 β†Ύt 𝐴) ∈ Conn)
185 rexanali 3103 . . . . . . . . . . 11 (βˆƒπ‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
186185rexbii 3095 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘¦ ∈ 𝐴 Β¬ βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
187 rexcom 3288 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
188 rexnal 3101 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ 𝐴 Β¬ βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
189186, 187, 1883bitr3i 301 . . . . . . . . 9 (βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
190189rexbii 3095 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘₯ ∈ 𝐴 Β¬ βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
191 rexcom 3288 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
192 rexnal 3101 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐴 Β¬ βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
193190, 191, 1923bitr3i 301 . . . . . . 7 (βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
194 r19.41v 3189 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ (βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
195194rexbii 3095 . . . . . . . . 9 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘₯ ∈ 𝐴 (βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
196 r19.41v 3189 . . . . . . . . 9 (βˆƒπ‘₯ ∈ 𝐴 (βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
197 reeanv 3227 . . . . . . . . . 10 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ↔ (βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦))
198197anbi1i 625 . . . . . . . . 9 ((βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
199195, 196, 1983bitri 297 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
200199rexbii 3095 . . . . . . 7 (βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
201193, 200bitr3i 277 . . . . . 6 (Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
20227ad2antrr 725 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ 𝐾 ∈ Toset)
20325sselda 3982 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ 𝐡)
204 simpllr 775 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ π‘Ÿ ∈ 𝐡)
20517, 10trleile 32129 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) β†’ (π‘₯ ≀ π‘Ÿ ∨ π‘Ÿ ≀ π‘₯))
206202, 203, 204, 205syl3anc 1372 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ (π‘₯ ≀ π‘Ÿ ∨ π‘Ÿ ≀ π‘₯))
207 simpr 486 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ 𝐴)
208 simplr 768 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ Β¬ π‘Ÿ ∈ 𝐴)
209 nelne2 3041 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ 𝐴 ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ π‘₯ β‰  π‘Ÿ)
210207, 208, 209syl2anc 585 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ β‰  π‘Ÿ)
211159adantr 482 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ 𝐾 ∈ Poset)
21217, 10posrasymb 32123 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) β†’ ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯) ↔ π‘₯ = π‘Ÿ))
213212necon3bbid 2979 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) β†’ (Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯) ↔ π‘₯ β‰  π‘Ÿ))
214211, 203, 204, 213syl3anc 1372 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ (Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯) ↔ π‘₯ β‰  π‘Ÿ))
215210, 214mpbird 257 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯))
216206, 215jca 513 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ ((π‘₯ ≀ π‘Ÿ ∨ π‘Ÿ ≀ π‘₯) ∧ Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯)))
217 pm5.17 1011 . . . . . . . . . . . 12 (((π‘₯ ≀ π‘Ÿ ∨ π‘Ÿ ≀ π‘₯) ∧ Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯)) ↔ (π‘₯ ≀ π‘Ÿ ↔ Β¬ π‘Ÿ ≀ π‘₯))
218216, 217sylib 217 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ (π‘₯ ≀ π‘Ÿ ↔ Β¬ π‘Ÿ ≀ π‘₯))
219218rexbidva 3177 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ↔ βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯))
22027ad2antrr 725 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝐾 ∈ Toset)
221 simpllr 775 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ π‘Ÿ ∈ 𝐡)
22225sselda 3982 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝑦 ∈ 𝐡)
22317, 10trleile 32129 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ (π‘Ÿ ≀ 𝑦 ∨ 𝑦 ≀ π‘Ÿ))
224220, 221, 222, 223syl3anc 1372 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ (π‘Ÿ ≀ 𝑦 ∨ 𝑦 ≀ π‘Ÿ))
225 simpr 486 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝑦 ∈ 𝐴)
226 simplr 768 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ Β¬ π‘Ÿ ∈ 𝐴)
227 nelne2 3041 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ 𝐴 ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝑦 β‰  π‘Ÿ)
228225, 226, 227syl2anc 585 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝑦 β‰  π‘Ÿ)
229228necomd 2997 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ π‘Ÿ β‰  𝑦)
230159adantr 482 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝐾 ∈ Poset)
23117, 10posrasymb 32123 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ ((π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ) ↔ π‘Ÿ = 𝑦))
232231necon3bbid 2979 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ (Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ) ↔ π‘Ÿ β‰  𝑦))
233230, 221, 222, 232syl3anc 1372 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ (Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ) ↔ π‘Ÿ β‰  𝑦))
234229, 233mpbird 257 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ))
235224, 234jca 513 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ ((π‘Ÿ ≀ 𝑦 ∨ 𝑦 ≀ π‘Ÿ) ∧ Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ)))
236 pm5.17 1011 . . . . . . . . . . . 12 (((π‘Ÿ ≀ 𝑦 ∨ 𝑦 ≀ π‘Ÿ) ∧ Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ)) ↔ (π‘Ÿ ≀ 𝑦 ↔ Β¬ 𝑦 ≀ π‘Ÿ))
237235, 236sylib 217 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ (π‘Ÿ ≀ 𝑦 ↔ Β¬ 𝑦 ≀ π‘Ÿ))
238237rexbidva 3177 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦 ↔ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ))
239219, 238anbi12d 632 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ↔ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)))
240239ex 414 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ (Β¬ π‘Ÿ ∈ 𝐴 β†’ ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ↔ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ))))
241240pm5.32rd 579 . . . . . . 7 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ (((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)))
242241rexbidva 3177 . . . . . 6 ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) β†’ (βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)))
243201, 242bitrid 283 . . . . 5 ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) β†’ (Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)))
244243biimpa 478 . . . 4 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)) β†’ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴))
2456, 184, 244r19.29af 3266 . . 3 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)) β†’ Β¬ (𝐽 β†Ύt 𝐴) ∈ Conn)
246245ex 414 . 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 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  {csn 4628   class class class wbr 5148   ↦ cmpt 5231   Γ— cxp 5674  dom cdm 5676  ran crn 5677  β€˜cfv 6541  (class class class)co 7406  ficfi 9402  Basecbs 17141  lecple 17201   β†Ύt crest 17363  topGenctg 17380  ordTopcordt 17442   Proset cproset 18243  Posetcpo 18257  Tosetctos 18366  TopOnctopon 22404  Conncconn 22907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-1o 8463  df-er 8700  df-en 8937  df-fin 8940  df-fi 9403  df-rest 17365  df-topgen 17386  df-ordt 17444  df-proset 18245  df-poset 18263  df-toset 18367  df-top 22388  df-topon 22405  df-bases 22441  df-cld 22515  df-conn 22908
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator