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