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 
|- B = ( Base ` K )
ordtconn.l 
|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
ordtconn.j 
|- J = ( ordTop ` .<_ )
Assertion ordtconnlem1 
|- ( ( K e. Toset /\ A C_ B ) -> ( ( J |`t A ) e. Conn -> A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) ) )

Proof

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