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 33393
Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 33394. See also reconnlem1 24664. (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 1909 . . . . 5 β„²π‘Ÿ(𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡)
2 nfcv 2895 . . . . . . 7 β„²π‘Ÿπ΄
3 nfra2w 3288 . . . . . . 7 β„²π‘Ÿβˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)
42, 3nfralw 3300 . . . . . 6 β„²π‘Ÿβˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)
54nfn 1852 . . . . 5 β„²π‘Ÿ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)
61, 5nfan 1894 . . . 4 β„²π‘Ÿ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
7 tospos 18375 . . . . . . . . . 10 (𝐾 ∈ Toset β†’ 𝐾 ∈ Poset)
8 posprs 18271 . . . . . . . . . 10 (𝐾 ∈ Poset β†’ 𝐾 ∈ Proset )
9 ordtconn.j . . . . . . . . . . 11 𝐽 = (ordTopβ€˜ ≀ )
10 ordtconn.l . . . . . . . . . . . . . 14 ≀ = ((leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡))
11 fvex 6894 . . . . . . . . . . . . . . 15 (leβ€˜πΎ) ∈ V
1211inex1 5307 . . . . . . . . . . . . . 14 ((leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡)) ∈ V
1310, 12eqeltri 2821 . . . . . . . . . . . . 13 ≀ ∈ V
14 eqid 2724 . . . . . . . . . . . . . 14 dom ≀ = dom ≀
1514ordttopon 23019 . . . . . . . . . . . . 13 ( ≀ ∈ V β†’ (ordTopβ€˜ ≀ ) ∈ (TopOnβ€˜dom ≀ ))
1613, 15ax-mp 5 . . . . . . . . . . . 12 (ordTopβ€˜ ≀ ) ∈ (TopOnβ€˜dom ≀ )
17 ordtconn.x . . . . . . . . . . . . . 14 𝐡 = (Baseβ€˜πΎ)
1817, 10prsdm 33383 . . . . . . . . . . . . 13 (𝐾 ∈ Proset β†’ dom ≀ = 𝐡)
1918fveq2d 6885 . . . . . . . . . . . 12 (𝐾 ∈ Proset β†’ (TopOnβ€˜dom ≀ ) = (TopOnβ€˜π΅))
2016, 19eleqtrid 2831 . . . . . . . . . . 11 (𝐾 ∈ Proset β†’ (ordTopβ€˜ ≀ ) ∈ (TopOnβ€˜π΅))
219, 20eqeltrid 2829 . . . . . . . . . 10 (𝐾 ∈ Proset β†’ 𝐽 ∈ (TopOnβ€˜π΅))
227, 8, 213syl 18 . . . . . . . . 9 (𝐾 ∈ Toset β†’ 𝐽 ∈ (TopOnβ€˜π΅))
2322ad3antrrr 727 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐽 ∈ (TopOnβ€˜π΅))
2423adantlr 712 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐽 ∈ (TopOnβ€˜π΅))
25 simpllr 773 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐴 βŠ† 𝐡)
2625adantlr 712 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐴 βŠ† 𝐡)
27 simpll 764 . . . . . . . . . . . 12 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ 𝐾 ∈ Toset)
2827, 7, 83syl 18 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ 𝐾 ∈ Proset )
29 snex 5421 . . . . . . . . . . . . . . . 16 {𝐡} ∈ V
3017fvexi 6895 . . . . . . . . . . . . . . . . . . 19 𝐡 ∈ V
3130mptex 7216 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) ∈ V
3231rnex 7896 . . . . . . . . . . . . . . . . 17 ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) ∈ V
3330mptex 7216 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) ∈ V
3433rnex 7896 . . . . . . . . . . . . . . . . 17 ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) ∈ V
3532, 34unex 7726 . . . . . . . . . . . . . . . 16 (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})) ∈ V
3629, 35unex 7726 . . . . . . . . . . . . . . 15 ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) ∈ V
37 ssfii 9410 . . . . . . . . . . . . . . 15 (({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) ∈ V β†’ ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) βŠ† (fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})))))
3836, 37ax-mp 5 . . . . . . . . . . . . . 14 ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) βŠ† (fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))))
39 fvex 6894 . . . . . . . . . . . . . . 15 (fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})))) ∈ V
40 bastg 22791 . . . . . . . . . . . . . . 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 3983 . . . . . . . . . . . . 13 ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) βŠ† (topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})))))
43 eqid 2724 . . . . . . . . . . . . . . 15 ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) = ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
44 eqid 2724 . . . . . . . . . . . . . . 15 ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) = ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
4517, 10, 43, 44ordtprsval 33387 . . . . . . . . . . . . . 14 (𝐾 ∈ Proset β†’ (ordTopβ€˜ ≀ ) = (topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))))))
469, 45eqtrid 2776 . . . . . . . . . . . . 13 (𝐾 ∈ Proset β†’ 𝐽 = (topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))))))
4742, 46sseqtrrid 4027 . . . . . . . . . . . 12 (𝐾 ∈ Proset β†’ ({𝐡} βˆͺ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))) βŠ† 𝐽)
4847unssbd 4180 . . . . . . . . . . 11 (𝐾 ∈ Proset β†’ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})) βŠ† 𝐽)
4928, 48syl 17 . . . . . . . . . 10 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ (ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βˆͺ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})) βŠ† 𝐽)
5049unssbd 4180 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) βŠ† 𝐽)
51 breq2 5142 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 β†’ (π‘Ÿ ≀ 𝑧 ↔ π‘Ÿ ≀ 𝑦))
5251notbid 318 . . . . . . . . . . . . 13 (𝑧 = 𝑦 β†’ (Β¬ π‘Ÿ ≀ 𝑧 ↔ Β¬ π‘Ÿ ≀ 𝑦))
5352cbvrabv 3434 . . . . . . . . . . . 12 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑦}
54 breq1 5141 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ÿ β†’ (π‘₯ ≀ 𝑦 ↔ π‘Ÿ ≀ 𝑦))
5554notbid 318 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ÿ β†’ (Β¬ π‘₯ ≀ 𝑦 ↔ Β¬ π‘Ÿ ≀ 𝑦))
5655rabbidv 3432 . . . . . . . . . . . . 13 (π‘₯ = π‘Ÿ β†’ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑦})
5756rspceeqv 3625 . . . . . . . . . . . 12 ((π‘Ÿ ∈ 𝐡 ∧ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑦}) β†’ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
5853, 57mpan2 688 . . . . . . . . . . 11 (π‘Ÿ ∈ 𝐡 β†’ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
5930rabex 5322 . . . . . . . . . . . 12 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ V
60 eqid 2724 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) = (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
6160elrnmpt 5945 . . . . . . . . . . . 12 ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ V β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) ↔ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))
6259, 61ax-mp 5 . . . . . . . . . . 11 ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}) ↔ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} = {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦})
6358, 62sylibr 233 . . . . . . . . . 10 (π‘Ÿ ∈ 𝐡 β†’ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))
6463adantl 481 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ π‘₯ ≀ 𝑦}))
6550, 64sseldd 3975 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ 𝐽)
6665ad2antrr 723 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∈ 𝐽)
6749unssad 4179 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) βŠ† 𝐽)
68 breq1 5141 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 β†’ (𝑧 ≀ π‘Ÿ ↔ 𝑦 ≀ π‘Ÿ))
6968notbid 318 . . . . . . . . . . . . 13 (𝑧 = 𝑦 β†’ (Β¬ 𝑧 ≀ π‘Ÿ ↔ Β¬ 𝑦 ≀ π‘Ÿ))
7069cbvrabv 3434 . . . . . . . . . . . 12 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘Ÿ}
71 breq2 5142 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ÿ β†’ (𝑦 ≀ π‘₯ ↔ 𝑦 ≀ π‘Ÿ))
7271notbid 318 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ÿ β†’ (Β¬ 𝑦 ≀ π‘₯ ↔ Β¬ 𝑦 ≀ π‘Ÿ))
7372rabbidv 3432 . . . . . . . . . . . . 13 (π‘₯ = π‘Ÿ β†’ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘Ÿ})
7473rspceeqv 3625 . . . . . . . . . . . 12 ((π‘Ÿ ∈ 𝐡 ∧ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘Ÿ}) β†’ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
7570, 74mpan2 688 . . . . . . . . . . 11 (π‘Ÿ ∈ 𝐡 β†’ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
7630rabex 5322 . . . . . . . . . . . 12 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ V
77 eqid 2724 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) = (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
7877elrnmpt 5945 . . . . . . . . . . . 12 ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ V β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) ↔ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}))
7976, 78ax-mp 5 . . . . . . . . . . 11 ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}) ↔ βˆƒπ‘₯ ∈ 𝐡 {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} = {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯})
8075, 79sylibr 233 . . . . . . . . . 10 (π‘Ÿ ∈ 𝐡 β†’ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}))
8180adantl 481 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ ran (π‘₯ ∈ 𝐡 ↦ {𝑦 ∈ 𝐡 ∣ Β¬ 𝑦 ≀ π‘₯}))
8267, 81sseldd 3975 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ 𝐽)
8382ad2antrr 723 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∈ 𝐽)
84 simpll 764 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡))
85 simpr 484 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ Β¬ π‘Ÿ ∈ 𝐴)
8684, 85jca 511 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴))
87 simplrl 774 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯)
88 ssel 3967 . . . . . . . . . . . . . . 15 (𝐴 βŠ† 𝐡 β†’ (π‘₯ ∈ 𝐴 β†’ π‘₯ ∈ 𝐡))
8988ancrd 551 . . . . . . . . . . . . . 14 (𝐴 βŠ† 𝐡 β†’ (π‘₯ ∈ 𝐴 β†’ (π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴)))
9089anim1d 610 . . . . . . . . . . . . 13 (𝐴 βŠ† 𝐡 β†’ ((π‘₯ ∈ 𝐴 ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ ((π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯)))
9190impl 455 . . . . . . . . . . . 12 (((𝐴 βŠ† 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ ((π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯))
92 elin 3956 . . . . . . . . . . . . 13 (π‘₯ ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) ↔ (π‘₯ ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∧ π‘₯ ∈ 𝐴))
93 breq2 5142 . . . . . . . . . . . . . . . 16 (𝑧 = π‘₯ β†’ (π‘Ÿ ≀ 𝑧 ↔ π‘Ÿ ≀ π‘₯))
9493notbid 318 . . . . . . . . . . . . . . 15 (𝑧 = π‘₯ β†’ (Β¬ π‘Ÿ ≀ 𝑧 ↔ Β¬ π‘Ÿ ≀ π‘₯))
9594elrab 3675 . . . . . . . . . . . . . 14 (π‘₯ ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ↔ (π‘₯ ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ π‘₯))
9695anbi1i 623 . . . . . . . . . . . . 13 ((π‘₯ ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∧ π‘₯ ∈ 𝐴) ↔ ((π‘₯ ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ π‘₯) ∧ π‘₯ ∈ 𝐴))
97 an32 643 . . . . . . . . . . . . 13 (((π‘₯ ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ π‘₯) ∧ π‘₯ ∈ 𝐴) ↔ ((π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯))
9892, 96, 973bitri 297 . . . . . . . . . . . 12 (π‘₯ ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) ↔ ((π‘₯ ∈ 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯))
9991, 98sylibr 233 . . . . . . . . . . 11 (((𝐴 βŠ† 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ π‘₯ ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴))
10099ne0d 4327 . . . . . . . . . 10 (((𝐴 βŠ† 𝐡 ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) β‰  βˆ…)
10125, 100sylanl1 677 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ π‘₯) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) β‰  βˆ…)
102101r19.29an 3150 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) β‰  βˆ…)
10386, 87, 102syl2anc 583 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ 𝐴) β‰  βˆ…)
104 simplrr 775 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)
105 ssel 3967 . . . . . . . . . . . . . . 15 (𝐴 βŠ† 𝐡 β†’ (𝑦 ∈ 𝐴 β†’ 𝑦 ∈ 𝐡))
106105ancrd 551 . . . . . . . . . . . . . 14 (𝐴 βŠ† 𝐡 β†’ (𝑦 ∈ 𝐴 β†’ (𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴)))
107106anim1d 610 . . . . . . . . . . . . 13 (𝐴 βŠ† 𝐡 β†’ ((𝑦 ∈ 𝐴 ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ ((𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ)))
108107impl 455 . . . . . . . . . . . 12 (((𝐴 βŠ† 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ ((𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ))
109 elin 3956 . . . . . . . . . . . . 13 (𝑦 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) ↔ (𝑦 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∧ 𝑦 ∈ 𝐴))
11069elrab 3675 . . . . . . . . . . . . . 14 (𝑦 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ↔ (𝑦 ∈ 𝐡 ∧ Β¬ 𝑦 ≀ π‘Ÿ))
111110anbi1i 623 . . . . . . . . . . . . 13 ((𝑦 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐡 ∧ Β¬ 𝑦 ≀ π‘Ÿ) ∧ 𝑦 ∈ 𝐴))
112 an32 643 . . . . . . . . . . . . 13 (((𝑦 ∈ 𝐡 ∧ Β¬ 𝑦 ≀ π‘Ÿ) ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ))
113109, 111, 1123bitri 297 . . . . . . . . . . . 12 (𝑦 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) ↔ ((𝑦 ∈ 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ))
114108, 113sylibr 233 . . . . . . . . . . 11 (((𝐴 βŠ† 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ 𝑦 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴))
115114ne0d 4327 . . . . . . . . . 10 (((𝐴 βŠ† 𝐡 ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) β‰  βˆ…)
11625, 115sylanl1 677 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ Β¬ 𝑦 ≀ π‘Ÿ) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) β‰  βˆ…)
117116r19.29an 3150 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) β‰  βˆ…)
11886, 104, 117syl2anc 583 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ∩ 𝐴) β‰  βˆ…)
11917, 10trleile 32608 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (π‘Ÿ ≀ 𝑧 ∨ 𝑧 ≀ π‘Ÿ))
120 oran 986 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ≀ 𝑧 ∨ 𝑧 ≀ π‘Ÿ) ↔ Β¬ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
121119, 120sylib 217 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ Β¬ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
1221213expa 1115 . . . . . . . . . . . . . 14 (((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ Β¬ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
123122nrexdv 3141 . . . . . . . . . . . . 13 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡) β†’ Β¬ βˆƒπ‘§ ∈ 𝐡 (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
124 rabid 3444 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ↔ (𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧))
125 rabid 3444 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ} ↔ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
126124, 125anbi12i 626 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ ((𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧) ∧ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
127 elin 3956 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
128 anandi 673 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ)) ↔ ((𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧) ∧ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
129126, 127, 1283bitr4i 303 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ (𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
130129exbii 1842 . . . . . . . . . . . . . . 15 (βˆƒπ‘§ 𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ βˆƒπ‘§(𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
131 nfrab1 3443 . . . . . . . . . . . . . . . . 17 Ⅎ𝑧{𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧}
132 nfrab1 3443 . . . . . . . . . . . . . . . . 17 Ⅎ𝑧{𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}
133131, 132nfin 4208 . . . . . . . . . . . . . . . 16 Ⅎ𝑧({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ})
134133n0f 4334 . . . . . . . . . . . . . . 15 (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) β‰  βˆ… ↔ βˆƒπ‘§ 𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
135 df-rex 3063 . . . . . . . . . . . . . . 15 (βˆƒπ‘§ ∈ 𝐡 (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ) ↔ βˆƒπ‘§(𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
136130, 134, 1353bitr4i 303 . . . . . . . . . . . . . 14 (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) β‰  βˆ… ↔ βˆƒπ‘§ ∈ 𝐡 (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ))
137136necon1bbii 2982 . . . . . . . . . . . . 13 (Β¬ βˆƒπ‘§ ∈ 𝐡 (Β¬ π‘Ÿ ≀ 𝑧 ∧ Β¬ 𝑧 ≀ π‘Ÿ) ↔ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = βˆ…)
138123, 137sylib 217 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = βˆ…)
139138adantlr 712 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = βˆ…)
140139adantr 480 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = βˆ…)
141140ineq1d 4203 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ∩ 𝐴) = (βˆ… ∩ 𝐴))
142 0in 4385 . . . . . . . . 9 (βˆ… ∩ 𝐴) = βˆ…
143141, 142eqtrdi 2780 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ∩ 𝐴) = βˆ…)
144143adantlr 712 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∩ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ∩ 𝐴) = βˆ…)
145 simplr 766 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ π‘Ÿ ∈ 𝐡)
146 simpr 484 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ Β¬ π‘Ÿ ∈ 𝐴)
147 vex 3470 . . . . . . . . . . . . . . 15 π‘Ÿ ∈ V
148147snss 4781 . . . . . . . . . . . . . 14 (π‘Ÿ ∈ 𝐡 ↔ {π‘Ÿ} βŠ† 𝐡)
149 eldif 3950 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ (𝐡 βˆ– 𝐴) ↔ (π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴))
150147snss 4781 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ (𝐡 βˆ– 𝐴) ↔ {π‘Ÿ} βŠ† (𝐡 βˆ– 𝐴))
151149, 150bitr3i 277 . . . . . . . . . . . . . . 15 ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ {π‘Ÿ} βŠ† (𝐡 βˆ– 𝐴))
152 ssconb 4129 . . . . . . . . . . . . . . 15 (({π‘Ÿ} βŠ† 𝐡 ∧ 𝐴 βŠ† 𝐡) β†’ ({π‘Ÿ} βŠ† (𝐡 βˆ– 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
153151, 152bitrid 283 . . . . . . . . . . . . . 14 (({π‘Ÿ} βŠ† 𝐡 ∧ 𝐴 βŠ† 𝐡) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
154148, 153sylanb 580 . . . . . . . . . . . . 13 ((π‘Ÿ ∈ 𝐡 ∧ 𝐴 βŠ† 𝐡) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
155154adantl 481 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ (π‘Ÿ ∈ 𝐡 ∧ 𝐴 βŠ† 𝐡)) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
156155anass1rs 652 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
157156adantr 480 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ((π‘Ÿ ∈ 𝐡 ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ})))
158145, 146, 157mpbi2and 709 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐴 βŠ† (𝐡 βˆ– {π‘Ÿ}))
1597ad3antrrr 727 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐾 ∈ Poset)
160 nfv 1909 . . . . . . . . . . 11 Ⅎ𝑧(𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡)
161131, 132nfun 4157 . . . . . . . . . . 11 Ⅎ𝑧({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ})
162 nfcv 2895 . . . . . . . . . . 11 Ⅎ𝑧(𝐡 βˆ– {π‘Ÿ})
163 ianor 978 . . . . . . . . . . . . . . 15 (Β¬ (π‘Ÿ ≀ 𝑧 ∧ 𝑧 ≀ π‘Ÿ) ↔ (Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ))
16417, 10posrasymb 32602 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ ((π‘Ÿ ≀ 𝑧 ∧ 𝑧 ≀ π‘Ÿ) ↔ π‘Ÿ = 𝑧))
165 equcom 2013 . . . . . . . . . . . . . . . . 17 (π‘Ÿ = 𝑧 ↔ 𝑧 = π‘Ÿ)
166164, 165bitrdi 287 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ ((π‘Ÿ ≀ 𝑧 ∧ 𝑧 ≀ π‘Ÿ) ↔ 𝑧 = π‘Ÿ))
167166necon3bbid 2970 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (Β¬ (π‘Ÿ ≀ 𝑧 ∧ 𝑧 ≀ π‘Ÿ) ↔ 𝑧 β‰  π‘Ÿ))
168163, 167bitr3id 285 . . . . . . . . . . . . . 14 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ ((Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ) ↔ 𝑧 β‰  π‘Ÿ))
1691683expia 1118 . . . . . . . . . . . . 13 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡) β†’ (𝑧 ∈ 𝐡 β†’ ((Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ) ↔ 𝑧 β‰  π‘Ÿ)))
170169pm5.32d 576 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡) β†’ ((𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ)) ↔ (𝑧 ∈ 𝐡 ∧ 𝑧 β‰  π‘Ÿ)))
171124, 125orbi12i 911 . . . . . . . . . . . . 13 ((𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ ((𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧) ∨ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
172 elun 4140 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
173 andi 1004 . . . . . . . . . . . . 13 ((𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ)) ↔ ((𝑧 ∈ 𝐡 ∧ Β¬ π‘Ÿ ≀ 𝑧) ∨ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ≀ π‘Ÿ)))
174171, 172, 1733bitr4ri 304 . . . . . . . . . . . 12 ((𝑧 ∈ 𝐡 ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∨ Β¬ 𝑧 ≀ π‘Ÿ)) ↔ 𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
175 eldifsn 4782 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐡 βˆ– {π‘Ÿ}) ↔ (𝑧 ∈ 𝐡 ∧ 𝑧 β‰  π‘Ÿ))
176175bicomi 223 . . . . . . . . . . . 12 ((𝑧 ∈ 𝐡 ∧ 𝑧 β‰  π‘Ÿ) ↔ 𝑧 ∈ (𝐡 βˆ– {π‘Ÿ}))
177170, 174, 1763bitr3g 313 . . . . . . . . . . 11 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡) β†’ (𝑧 ∈ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) ↔ 𝑧 ∈ (𝐡 βˆ– {π‘Ÿ})))
178160, 161, 162, 177eqrd 3993 . . . . . . . . . 10 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = (𝐡 βˆ– {π‘Ÿ}))
179159, 145, 178syl2anc 583 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}) = (𝐡 βˆ– {π‘Ÿ}))
180158, 179sseqtrrd 4015 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐴 βŠ† ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
181180adantlr 712 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝐴 βŠ† ({𝑧 ∈ 𝐡 ∣ Β¬ π‘Ÿ ≀ 𝑧} βˆͺ {𝑧 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ π‘Ÿ}))
18224, 26, 66, 83, 103, 118, 144, 181nconnsubb 23249 . . . . . 6 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ Β¬ (𝐽 β†Ύt 𝐴) ∈ Conn)
183182anasss 466 . . . . 5 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)) β†’ Β¬ (𝐽 β†Ύt 𝐴) ∈ Conn)
184183adantllr 716 . . . 4 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)) ∧ π‘Ÿ ∈ 𝐡) ∧ ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)) β†’ Β¬ (𝐽 β†Ύt 𝐴) ∈ Conn)
185 rexanali 3094 . . . . . . . . . . 11 (βˆƒπ‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
186185rexbii 3086 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘¦ ∈ 𝐴 Β¬ βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
187 rexcom 3279 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
188 rexnal 3092 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ 𝐴 Β¬ βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
189186, 187, 1883bitr3i 301 . . . . . . . . 9 (βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
190189rexbii 3086 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘₯ ∈ 𝐴 Β¬ βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
191 rexcom 3279 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
192 rexnal 3092 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐴 Β¬ βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
193190, 191, 1923bitr3i 301 . . . . . . 7 (βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴))
194 r19.41v 3180 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ (βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
195194rexbii 3086 . . . . . . . . 9 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘₯ ∈ 𝐴 (βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
196 r19.41v 3180 . . . . . . . . 9 (βˆƒπ‘₯ ∈ 𝐴 (βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
197 reeanv 3218 . . . . . . . . . 10 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ↔ (βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦))
198197anbi1i 623 . . . . . . . . 9 ((βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
199195, 196, 1983bitri 297 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
200199rexbii 3086 . . . . . . 7 (βˆƒπ‘Ÿ ∈ 𝐡 βˆƒπ‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
201193, 200bitr3i 277 . . . . . 6 (Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴))
20227ad2antrr 723 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ 𝐾 ∈ Toset)
20325sselda 3974 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ 𝐡)
204 simpllr 773 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ π‘Ÿ ∈ 𝐡)
20517, 10trleile 32608 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) β†’ (π‘₯ ≀ π‘Ÿ ∨ π‘Ÿ ≀ π‘₯))
206202, 203, 204, 205syl3anc 1368 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ (π‘₯ ≀ π‘Ÿ ∨ π‘Ÿ ≀ π‘₯))
207 simpr 484 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ 𝐴)
208 simplr 766 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ Β¬ π‘Ÿ ∈ 𝐴)
209 nelne2 3032 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ 𝐴 ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ π‘₯ β‰  π‘Ÿ)
210207, 208, 209syl2anc 583 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ β‰  π‘Ÿ)
211159adantr 480 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ 𝐾 ∈ Poset)
21217, 10posrasymb 32602 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) β†’ ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯) ↔ π‘₯ = π‘Ÿ))
213212necon3bbid 2970 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ π‘₯ ∈ 𝐡 ∧ π‘Ÿ ∈ 𝐡) β†’ (Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯) ↔ π‘₯ β‰  π‘Ÿ))
214211, 203, 204, 213syl3anc 1368 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ (Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯) ↔ π‘₯ β‰  π‘Ÿ))
215210, 214mpbird 257 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯))
216206, 215jca 511 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ ((π‘₯ ≀ π‘Ÿ ∨ π‘Ÿ ≀ π‘₯) ∧ Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯)))
217 pm5.17 1008 . . . . . . . . . . . 12 (((π‘₯ ≀ π‘Ÿ ∨ π‘Ÿ ≀ π‘₯) ∧ Β¬ (π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ π‘₯)) ↔ (π‘₯ ≀ π‘Ÿ ↔ Β¬ π‘Ÿ ≀ π‘₯))
218216, 217sylib 217 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ π‘₯ ∈ 𝐴) β†’ (π‘₯ ≀ π‘Ÿ ↔ Β¬ π‘Ÿ ≀ π‘₯))
219218rexbidva 3168 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ↔ βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯))
22027ad2antrr 723 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝐾 ∈ Toset)
221 simpllr 773 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ π‘Ÿ ∈ 𝐡)
22225sselda 3974 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝑦 ∈ 𝐡)
22317, 10trleile 32608 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ (π‘Ÿ ≀ 𝑦 ∨ 𝑦 ≀ π‘Ÿ))
224220, 221, 222, 223syl3anc 1368 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ (π‘Ÿ ≀ 𝑦 ∨ 𝑦 ≀ π‘Ÿ))
225 simpr 484 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝑦 ∈ 𝐴)
226 simplr 766 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ Β¬ π‘Ÿ ∈ 𝐴)
227 nelne2 3032 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ 𝐴 ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ 𝑦 β‰  π‘Ÿ)
228225, 226, 227syl2anc 583 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝑦 β‰  π‘Ÿ)
229228necomd 2988 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ π‘Ÿ β‰  𝑦)
230159adantr 480 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ 𝐾 ∈ Poset)
23117, 10posrasymb 32602 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ ((π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ) ↔ π‘Ÿ = 𝑦))
232231necon3bbid 2970 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ π‘Ÿ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ (Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ) ↔ π‘Ÿ β‰  𝑦))
233230, 221, 222, 232syl3anc 1368 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ (Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ) ↔ π‘Ÿ β‰  𝑦))
234229, 233mpbird 257 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ))
235224, 234jca 511 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ ((π‘Ÿ ≀ 𝑦 ∨ 𝑦 ≀ π‘Ÿ) ∧ Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ)))
236 pm5.17 1008 . . . . . . . . . . . 12 (((π‘Ÿ ≀ 𝑦 ∨ 𝑦 ≀ π‘Ÿ) ∧ Β¬ (π‘Ÿ ≀ 𝑦 ∧ 𝑦 ≀ π‘Ÿ)) ↔ (π‘Ÿ ≀ 𝑦 ↔ Β¬ 𝑦 ≀ π‘Ÿ))
237235, 236sylib 217 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ (π‘Ÿ ≀ 𝑦 ↔ Β¬ 𝑦 ≀ π‘Ÿ))
238237rexbidva 3168 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ (βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦 ↔ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ))
239219, 238anbi12d 630 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) ∧ Β¬ π‘Ÿ ∈ 𝐴) β†’ ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ↔ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ)))
240239ex 412 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ (Β¬ π‘Ÿ ∈ 𝐴 β†’ ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ↔ (βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ))))
241240pm5.32rd 577 . . . . . . 7 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ π‘Ÿ ∈ 𝐡) β†’ (((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)))
242241rexbidva 3168 . . . . . 6 ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) β†’ (βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ π‘Ÿ ∧ βˆƒπ‘¦ ∈ 𝐴 π‘Ÿ ≀ 𝑦) ∧ Β¬ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)))
243201, 242bitrid 283 . . . . 5 ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) β†’ (Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴) ↔ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴)))
244243biimpa 476 . . . 4 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)) β†’ βˆƒπ‘Ÿ ∈ 𝐡 ((βˆƒπ‘₯ ∈ 𝐴 Β¬ π‘Ÿ ≀ π‘₯ ∧ βˆƒπ‘¦ ∈ 𝐴 Β¬ 𝑦 ≀ π‘Ÿ) ∧ Β¬ π‘Ÿ ∈ 𝐴))
2456, 184, 244r19.29af 3257 . . 3 (((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) ∧ Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)) β†’ Β¬ (𝐽 β†Ύt 𝐴) ∈ Conn)
246245ex 412 . 2 ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) β†’ (Β¬ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴) β†’ Β¬ (𝐽 β†Ύt 𝐴) ∈ Conn))
247246con4d 115 1 ((𝐾 ∈ Toset ∧ 𝐴 βŠ† 𝐡) β†’ ((𝐽 β†Ύt 𝐴) ∈ Conn β†’ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘Ÿ ∈ 𝐡 ((π‘₯ ≀ π‘Ÿ ∧ π‘Ÿ ≀ 𝑦) β†’ π‘Ÿ ∈ 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∧ w3a 1084   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098   β‰  wne 2932  βˆ€wral 3053  βˆƒwrex 3062  {crab 3424  Vcvv 3466   βˆ– cdif 3937   βˆͺ cun 3938   ∩ cin 3939   βŠ† wss 3940  βˆ…c0 4314  {csn 4620   class class class wbr 5138   ↦ cmpt 5221   Γ— cxp 5664  dom cdm 5666  ran crn 5667  β€˜cfv 6533  (class class class)co 7401  ficfi 9401  Basecbs 17143  lecple 17203   β†Ύt crest 17365  topGenctg 17382  ordTopcordt 17444   Proset cproset 18248  Posetcpo 18262  Tosetctos 18371  TopOnctopon 22734  Conncconn 23237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-1o 8461  df-er 8699  df-en 8936  df-fin 8939  df-fi 9402  df-rest 17367  df-topgen 17388  df-ordt 17446  df-proset 18250  df-poset 18268  df-toset 18372  df-top 22718  df-topon 22735  df-bases 22771  df-cld 22845  df-conn 23238
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator