Metamath Proof Explorer

Theorem ordtconnlem1

Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn . See also reconnlem1 . (Contributed by Thierry Arnoux, 14-Sep-2018)

Ref Expression
Hypotheses ordtconn.x ⊢ 𝐵 = ( Base ‘ 𝐾 )
ordtconn.l ⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
ordtconn.j ⊢ 𝐽 = ( ordTop ‘ ≤ )
Assertion ordtconnlem1 ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 ordtconn.x ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ordtconn.l ⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
3 ordtconn.j ⊢ 𝐽 = ( ordTop ‘ ≤ )
4 nfv ⊢ Ⅎ 𝑟 ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 )
5 nfcv ⊢ Ⅎ 𝑟 𝐴
6 nfra2w ⊢ Ⅎ 𝑟 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 )
7 5 6 nfralw ⊢ Ⅎ 𝑟 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 )
8 7 nfn ⊢ Ⅎ 𝑟 ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 )
9 4 8 nfan ⊢ Ⅎ 𝑟 ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) )
10 tospos ⊢ ( 𝐾 ∈ Toset → 𝐾 ∈ Poset )
11 posprs ⊢ ( 𝐾 ∈ Poset → 𝐾 ∈ Proset )
12 fvex ⊢ ( le ‘ 𝐾 ) ∈ V
13 12 inex1 ⊢ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) ∈ V
14 2 13 eqeltri ⊢ ≤ ∈ V
15 eqid ⊢ dom ≤ = dom ≤
16 15 ordttopon ⊢ ( ≤ ∈ V → ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ dom ≤ ) )
17 14 16 ax-mp ⊢ ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ dom ≤ )
18 1 2 prsdm ⊢ ( 𝐾 ∈ Proset → dom ≤ = 𝐵 )
19 18 fveq2d ⊢ ( 𝐾 ∈ Proset → ( TopOn ‘ dom ≤ ) = ( TopOn ‘ 𝐵 ) )
20 17 19 eleqtrid ⊢ ( 𝐾 ∈ Proset → ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ 𝐵 ) )
21 3 20 eqeltrid ⊢ ( 𝐾 ∈ Proset → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
22 10 11 21 3syl ⊢ ( 𝐾 ∈ Toset → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
23 22 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
24 23 adantlr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
25 simpllr ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → 𝐴 ⊆ 𝐵 )
26 25 adantlr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → 𝐴 ⊆ 𝐵 )
27 simpll ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → 𝐾 ∈ Toset )
28 27 10 11 3syl ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → 𝐾 ∈ Proset )
29 snex ⊢ { 𝐵 } ∈ V
30 1 fvexi ⊢ 𝐵 ∈ V
31 30 mptex ⊢ ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∈ V
32 31 rnex ⊢ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∈ V
33 30 mptex ⊢ ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ∈ V
34 33 rnex ⊢ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ∈ V
35 32 34 unex ⊢ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ∈ V
36 29 35 unex ⊢ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ∈ V
37 ssfii ⊢ ( ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ∈ V → ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ⊆ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) )
38 36 37 ax-mp ⊢ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ⊆ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) )
39 fvex ⊢ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) ∈ V
40 bastg ⊢ ( ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) ∈ V → ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) ) )
41 39 40 ax-mp ⊢ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) )
42 38 41 sstri ⊢ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) )
43 eqid ⊢ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } )
44 eqid ⊢ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } )
45 1 2 43 44 ordtprsval ⊢ ( 𝐾 ∈ Proset → ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) ) )
46 3 45 syl5eq ⊢ ( 𝐾 ∈ Proset → 𝐽 = ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) ) )
47 42 46 sseqtrrid ⊢ ( 𝐾 ∈ Proset → ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ⊆ 𝐽 )
48 47 unssbd ⊢ ( 𝐾 ∈ Proset → ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ⊆ 𝐽 )
49 28 48 syl ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ⊆ 𝐽 )
50 49 unssbd ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ⊆ 𝐽 )
51 breq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑟 ≤ 𝑧 ↔ 𝑟 ≤ 𝑦 ) )
52 51 notbid ⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑟 ≤ 𝑧 ↔ ¬ 𝑟 ≤ 𝑦 ) )
53 52 cbvrabv ⊢ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦 }
54 breq1 ⊢ ( 𝑥 = 𝑟 → ( 𝑥 ≤ 𝑦 ↔ 𝑟 ≤ 𝑦 ) )
55 54 notbid ⊢ ( 𝑥 = 𝑟 → ( ¬ 𝑥 ≤ 𝑦 ↔ ¬ 𝑟 ≤ 𝑦 ) )
56 55 rabbidv ⊢ ( 𝑥 = 𝑟 → { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦 } )
57 56 rspceeqv ⊢ ( ( 𝑟 ∈ 𝐵 ∧ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦 } ) → ∃ 𝑥 ∈ 𝐵 { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } )
58 53 57 mpan2 ⊢ ( 𝑟 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐵 { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } )
59 30 rabex ⊢ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∈ V
60 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) = ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } )
61 60 elrnmpt ⊢ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∈ V → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∈ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ↔ ∃ 𝑥 ∈ 𝐵 { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) )
62 59 61 ax-mp ⊢ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∈ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ↔ ∃ 𝑥 ∈ 𝐵 { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } )
63 58 62 sylibr ⊢ ( 𝑟 ∈ 𝐵 → { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∈ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) )
64 63 adantl ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∈ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) )
65 50 64 sseldd ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∈ 𝐽 )
66 65 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∈ 𝐽 )
67 49 unssad ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ⊆ 𝐽 )
68 breq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ≤ 𝑟 ↔ 𝑦 ≤ 𝑟 ) )
69 68 notbid ⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑧 ≤ 𝑟 ↔ ¬ 𝑦 ≤ 𝑟 ) )
70 69 cbvrabv ⊢ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟 }
71 breq2 ⊢ ( 𝑥 = 𝑟 → ( 𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 𝑟 ) )
72 71 notbid ⊢ ( 𝑥 = 𝑟 → ( ¬ 𝑦 ≤ 𝑥 ↔ ¬ 𝑦 ≤ 𝑟 ) )
73 72 rabbidv ⊢ ( 𝑥 = 𝑟 → { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟 } )
74 73 rspceeqv ⊢ ( ( 𝑟 ∈ 𝐵 ∧ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟 } ) → ∃ 𝑥 ∈ 𝐵 { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } )
75 70 74 mpan2 ⊢ ( 𝑟 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐵 { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } )
76 30 rabex ⊢ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∈ V
77 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) = ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } )
78 77 elrnmpt ⊢ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∈ V → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∈ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝐵 { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) )
79 76 78 ax-mp ⊢ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∈ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝐵 { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } )
80 75 79 sylibr ⊢ ( 𝑟 ∈ 𝐵 → { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∈ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) )
81 80 adantl ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∈ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) )
82 67 81 sseldd ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∈ 𝐽 )
83 82 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∈ 𝐽 )
84 simpll ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) )
85 simpr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ¬ 𝑟 ∈ 𝐴 )
86 84 85 jca ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) )
87 simplrl ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 )
88 ssel ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
89 88 ancrd ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) )
90 89 anim1d ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑥 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝑟 ≤ 𝑥 ) ) )
91 90 impl ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝑟 ≤ 𝑥 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝑟 ≤ 𝑥 ) )
92 elin ⊢ ( 𝑥 ∈ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ 𝐴 ) ↔ ( 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∧ 𝑥 ∈ 𝐴 ) )
93 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑟 ≤ 𝑧 ↔ 𝑟 ≤ 𝑥 ) )
94 93 notbid ⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑟 ≤ 𝑧 ↔ ¬ 𝑟 ≤ 𝑥 ) )
95 94 elrab ⊢ ( 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥 ) )
96 95 anbi1i ⊢ ( ( 𝑥 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∧ 𝑥 ∈ 𝐴 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥 ) ∧ 𝑥 ∈ 𝐴 ) )
97 an32 ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥 ) ∧ 𝑥 ∈ 𝐴 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝑟 ≤ 𝑥 ) )
98 92 96 97 3bitri ⊢ ( 𝑥 ∈ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ 𝐴 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝑟 ≤ 𝑥 ) )
99 91 98 sylibr ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝑟 ≤ 𝑥 ) → 𝑥 ∈ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ 𝐴 ) )
100 99 ne0d ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝑟 ≤ 𝑥 ) → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ 𝐴 ) ≠ ∅ )
101 25 100 sylanl1 ⊢ ( ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝑟 ≤ 𝑥 ) → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ 𝐴 ) ≠ ∅ )
102 101 r19.29an ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ) → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ 𝐴 ) ≠ ∅ )
103 86 87 102 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ 𝐴 ) ≠ ∅ )
104 simplrr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 )
105 ssel ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) )
106 105 ancrd ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑦 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) )
107 106 anim1d ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑟 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ 𝑦 ≤ 𝑟 ) ) )
108 107 impl ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ 𝑦 ≤ 𝑟 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ 𝑦 ≤ 𝑟 ) )
109 elin ⊢ ( 𝑦 ∈ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∩ 𝐴 ) ↔ ( 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∧ 𝑦 ∈ 𝐴 ) )
110 69 elrab ⊢ ( 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟 ) )
111 110 anbi1i ⊢ ( ( 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∧ 𝑦 ∈ 𝐴 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟 ) ∧ 𝑦 ∈ 𝐴 ) )
112 an32 ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟 ) ∧ 𝑦 ∈ 𝐴 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ 𝑦 ≤ 𝑟 ) )
113 109 111 112 3bitri ⊢ ( 𝑦 ∈ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∩ 𝐴 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ 𝑦 ≤ 𝑟 ) )
114 108 113 sylibr ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ 𝑦 ≤ 𝑟 ) → 𝑦 ∈ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∩ 𝐴 ) )
115 114 ne0d ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ 𝑦 ≤ 𝑟 ) → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∩ 𝐴 ) ≠ ∅ )
116 25 115 sylanl1 ⊢ ( ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ 𝑦 ≤ 𝑟 ) → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∩ 𝐴 ) ≠ ∅ )
117 116 r19.29an ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∩ 𝐴 ) ≠ ∅ )
118 86 104 117 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ∩ 𝐴 ) ≠ ∅ )
119 1 2 trleile ⊢ ( ( 𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑟 ≤ 𝑧 ∨ 𝑧 ≤ 𝑟 ) )
120 oran ⊢ ( ( 𝑟 ≤ 𝑧 ∨ 𝑧 ≤ 𝑟 ) ↔ ¬ ( ¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟 ) )
121 119 120 sylib ⊢ ( ( 𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ¬ ( ¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟 ) )
122 121 3expa ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ¬ ( ¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟 ) )
123 122 nrexdv ⊢ ( ( 𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ) → ¬ ∃ 𝑧 ∈ 𝐵 ( ¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟 ) )
124 rabid ⊢ ( 𝑧 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ↔ ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧 ) )
125 rabid ⊢ ( 𝑧 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ↔ ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟 ) )
126 124 125 anbi12i ⊢ ( ( 𝑧 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∧ 𝑧 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) ↔ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧 ) ∧ ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟 ) ) )
127 elin ⊢ ( 𝑧 ∈ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) ↔ ( 𝑧 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∧ 𝑧 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) )
128 anandi ⊢ ( ( 𝑧 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟 ) ) ↔ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧 ) ∧ ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟 ) ) )
129 126 127 128 3bitr4i ⊢ ( 𝑧 ∈ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) ↔ ( 𝑧 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟 ) ) )
130 129 exbii ⊢ ( ∃ 𝑧 𝑧 ∈ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟 ) ) )
131 nfrab1 ⊢ Ⅎ 𝑧 { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 }
132 nfrab1 ⊢ Ⅎ 𝑧 { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 }
133 131 132 nfin ⊢ Ⅎ 𝑧 ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } )
134 133 n0f ⊢ ( ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) )
135 df-rex ⊢ ( ∃ 𝑧 ∈ 𝐵 ( ¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟 ) ) )
136 130 134 135 3bitr4i ⊢ ( ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) ≠ ∅ ↔ ∃ 𝑧 ∈ 𝐵 ( ¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟 ) )
137 136 necon1bbii ⊢ ( ¬ ∃ 𝑧 ∈ 𝐵 ( ¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟 ) ↔ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) = ∅ )
138 123 137 sylib ⊢ ( ( 𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ) → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) = ∅ )
139 138 adantlr ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) = ∅ )
140 139 adantr ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) = ∅ )
141 140 ineq1d ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ( ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) ∩ 𝐴 ) = ( ∅ ∩ 𝐴 ) )
142 0in ⊢ ( ∅ ∩ 𝐴 ) = ∅
143 141 142 eqtrdi ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ( ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) ∩ 𝐴 ) = ∅ )
144 143 adantlr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ( ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∩ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) ∩ 𝐴 ) = ∅ )
145 simplr ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → 𝑟 ∈ 𝐵 )
146 simpr ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ¬ 𝑟 ∈ 𝐴 )
147 vex ⊢ 𝑟 ∈ V
148 147 snss ⊢ ( 𝑟 ∈ 𝐵 ↔ { 𝑟 } ⊆ 𝐵 )
149 eldif ⊢ ( 𝑟 ∈ ( 𝐵 ∖ 𝐴 ) ↔ ( 𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴 ) )
150 147 snss ⊢ ( 𝑟 ∈ ( 𝐵 ∖ 𝐴 ) ↔ { 𝑟 } ⊆ ( 𝐵 ∖ 𝐴 ) )
151 149 150 bitr3i ⊢ ( ( 𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ { 𝑟 } ⊆ ( 𝐵 ∖ 𝐴 ) )
152 ssconb ⊢ ( ( { 𝑟 } ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵 ) → ( { 𝑟 } ⊆ ( 𝐵 ∖ 𝐴 ) ↔ 𝐴 ⊆ ( 𝐵 ∖ { 𝑟 } ) ) )
153 151 152 syl5bb ⊢ ( ( { 𝑟 } ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ 𝐴 ⊆ ( 𝐵 ∖ { 𝑟 } ) ) )
154 148 153 sylanb ⊢ ( ( 𝑟 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ 𝐴 ⊆ ( 𝐵 ∖ { 𝑟 } ) ) )
155 154 adantl ⊢ ( ( 𝐾 ∈ Toset ∧ ( 𝑟 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐵 ) ) → ( ( 𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ 𝐴 ⊆ ( 𝐵 ∖ { 𝑟 } ) ) )
156 155 anass1rs ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ 𝐴 ⊆ ( 𝐵 ∖ { 𝑟 } ) ) )
157 156 adantr ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ( ( 𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ 𝐴 ⊆ ( 𝐵 ∖ { 𝑟 } ) ) )
158 145 146 157 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → 𝐴 ⊆ ( 𝐵 ∖ { 𝑟 } ) )
159 10 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ Poset )
160 nfv ⊢ Ⅎ 𝑧 ( 𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 )
161 131 132 nfun ⊢ Ⅎ 𝑧 ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∪ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } )
162 nfcv ⊢ Ⅎ 𝑧 ( 𝐵 ∖ { 𝑟 } )
163 ianor ⊢ ( ¬ ( 𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟 ) ↔ ( ¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟 ) )
164 1 2 posrasymb ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟 ) ↔ 𝑟 = 𝑧 ) )
165 equcom ⊢ ( 𝑟 = 𝑧 ↔ 𝑧 = 𝑟 )
166 164 165 bitrdi ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟 ) ↔ 𝑧 = 𝑟 ) )
167 166 necon3bbid ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ¬ ( 𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟 ) ↔ 𝑧 ≠ 𝑟 ) )
168 163 167 bitr3id ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( ¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟 ) ↔ 𝑧 ≠ 𝑟 ) )
169 168 3expia ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ) → ( 𝑧 ∈ 𝐵 → ( ( ¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟 ) ↔ 𝑧 ≠ 𝑟 ) ) )
170 169 pm5.32d ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝑧 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟 ) ) ↔ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟 ) ) )
171 124 125 orbi12i ⊢ ( ( 𝑧 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∨ 𝑧 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) ↔ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧 ) ∨ ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟 ) ) )
172 elun ⊢ ( 𝑧 ∈ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∪ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) ↔ ( 𝑧 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∨ 𝑧 ∈ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) )
173 andi ⊢ ( ( 𝑧 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟 ) ) ↔ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧 ) ∨ ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟 ) ) )
174 171 172 173 3bitr4ri ⊢ ( ( 𝑧 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟 ) ) ↔ 𝑧 ∈ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∪ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) )
175 eldifsn ⊢ ( 𝑧 ∈ ( 𝐵 ∖ { 𝑟 } ) ↔ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟 ) )
176 175 bicomi ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟 ) ↔ 𝑧 ∈ ( 𝐵 ∖ { 𝑟 } ) )
177 170 174 176 3bitr3g ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ) → ( 𝑧 ∈ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∪ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) ↔ 𝑧 ∈ ( 𝐵 ∖ { 𝑟 } ) ) )
178 160 161 162 177 eqrd ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ) → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∪ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) = ( 𝐵 ∖ { 𝑟 } ) )
179 159 145 178 syl2anc ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∪ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) = ( 𝐵 ∖ { 𝑟 } ) )
180 158 179 sseqtrrd ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → 𝐴 ⊆ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∪ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) )
181 180 adantlr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → 𝐴 ⊆ ( { 𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧 } ∪ { 𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟 } ) )
182 24 26 66 83 103 118 144 181 nconnsubb ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ¬ ( 𝐽 ↾t 𝐴 ) ∈ Conn )
183 182 anasss ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ) → ¬ ( 𝐽 ↾t 𝐴 ) ∈ Conn )
184 183 adantllr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ) → ¬ ( 𝐽 ↾t 𝐴 ) ∈ Conn )
185 rexanali ⊢ ( ∃ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ¬ ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) )
186 185 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐴 ¬ ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) )
187 rexcom ⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) )
188 rexnal ⊢ ( ∃ 𝑦 ∈ 𝐴 ¬ ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) ↔ ¬ ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) )
189 186 187 188 3bitr3i ⊢ ( ∃ 𝑟 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ¬ ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) )
190 189 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑟 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) )
191 rexcom ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑟 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) )
192 rexnal ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) )
193 190 191 192 3bitr3i ⊢ ( ∃ 𝑟 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) )
194 r19.41v ⊢ ( ∃ 𝑦 ∈ 𝐴 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) )
195 194 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) )
196 r19.41v ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) )
197 reeanv ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃ 𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ) )
198 197 anbi1i ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ( ( ∃ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃ 𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) )
199 195 196 198 3bitri ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ( ( ∃ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃ 𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) )
200 199 rexbii ⊢ ( ∃ 𝑟 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 ( ( ∃ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃ 𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) )
201 193 200 bitr3i ⊢ ( ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 ( ( ∃ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃ 𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) )
202 27 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐾 ∈ Toset )
203 25 sselda ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
204 simpllr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑟 ∈ 𝐵 )
205 1 2 trleile ⊢ ( ( 𝐾 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) → ( 𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥 ) )
206 202 203 204 205 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥 ) )
207 simpr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
208 simplr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑟 ∈ 𝐴 )
209 nelne2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑟 ∈ 𝐴 ) → 𝑥 ≠ 𝑟 )
210 207 208 209 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ 𝑟 )
211 159 adantr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐾 ∈ Poset )
212 1 2 posrasymb ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥 ) ↔ 𝑥 = 𝑟 ) )
213 212 necon3bbid ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) → ( ¬ ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥 ) ↔ 𝑥 ≠ 𝑟 ) )
214 211 203 204 213 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥 ) ↔ 𝑥 ≠ 𝑟 ) )
215 210 214 mpbird ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ¬ ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥 ) )
216 206 215 jca ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥 ) ∧ ¬ ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥 ) ) )
217 pm5.17 ⊢ ( ( ( 𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥 ) ∧ ¬ ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥 ) ) ↔ ( 𝑥 ≤ 𝑟 ↔ ¬ 𝑟 ≤ 𝑥 ) )
218 216 217 sylib ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≤ 𝑟 ↔ ¬ 𝑟 ≤ 𝑥 ) )
219 218 rexbidva ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ↔ ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ) )
220 27 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝐾 ∈ Toset )
221 simpllr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑟 ∈ 𝐵 )
222 25 sselda ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 )
223 1 2 trleile ⊢ ( ( 𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟 ) )
224 220 221 222 223 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟 ) )
225 simpr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
226 simplr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ¬ 𝑟 ∈ 𝐴 )
227 nelne2 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑟 ∈ 𝐴 ) → 𝑦 ≠ 𝑟 )
228 225 226 227 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ≠ 𝑟 )
229 228 necomd ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑟 ≠ 𝑦 )
230 159 adantr ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝐾 ∈ Poset )
231 1 2 posrasymb ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟 ) ↔ 𝑟 = 𝑦 ) )
232 231 necon3bbid ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ¬ ( 𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟 ) ↔ 𝑟 ≠ 𝑦 ) )
233 230 221 222 232 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ¬ ( 𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟 ) ↔ 𝑟 ≠ 𝑦 ) )
234 229 233 mpbird ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ¬ ( 𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟 ) )
235 224 234 jca ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟 ) ∧ ¬ ( 𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟 ) ) )
236 pm5.17 ⊢ ( ( ( 𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟 ) ∧ ¬ ( 𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟 ) ) ↔ ( 𝑟 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑟 ) )
237 235 236 sylib ⊢ ( ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑟 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑟 ) )
238 237 rexbidva ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) )
239 219 238 anbi12d ⊢ ( ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ¬ 𝑟 ∈ 𝐴 ) → ( ( ∃ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃ 𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) )
240 239 ex ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → ( ¬ 𝑟 ∈ 𝐴 → ( ( ∃ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃ 𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ) ) )
241 240 pm5.32rd ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → ( ( ( ∃ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃ 𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ( ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ) )
242 241 rexbidva ⊢ ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) → ( ∃ 𝑟 ∈ 𝐵 ( ( ∃ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃ 𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 ( ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ) )
243 201 242 syl5bb ⊢ ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) → ( ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 ( ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ∧ ¬ 𝑟 ∈ 𝐴 ) ) )
244 243 biimpa ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) ) → ∃ 𝑟 ∈ 𝐵 ( ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟 ) ∧ ¬ 𝑟 ∈ 𝐴 ) )
245 9 184 244 r19.29af ⊢ ( ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) ∧ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) ) → ¬ ( 𝐽 ↾t 𝐴 ) ∈ Conn )
246 245 ex ⊢ ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) → ( ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) → ¬ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) )
247 246 con4d ⊢ ( ( 𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ( 𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦 ) → 𝑟 ∈ 𝐴 ) ) )