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 27 10 11 3syl 
 |-  ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> K e. Proset )
29 snex 
 |-  { B } e. _V
30 1 fvexi 
 |-  B e. _V
31 30 mptex 
 |-  ( x e. B |-> { y e. B | -. y .<_ x } ) e. _V
32 31 rnex 
 |-  ran ( x e. B |-> { y e. B | -. y .<_ x } ) e. _V
33 30 mptex 
 |-  ( x e. B |-> { y e. B | -. x .<_ y } ) e. _V
34 33 rnex 
 |-  ran ( x e. B |-> { y e. B | -. x .<_ y } ) e. _V
35 32 34 unex 
 |-  ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) e. _V
36 29 35 unex 
 |-  ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) e. _V
37 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 } ) ) ) ) )
38 36 37 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 } ) ) ) )
39 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
40 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 } ) ) ) ) ) )
41 39 40 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 } ) ) ) ) )
42 38 41 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 } ) ) ) ) )
43 eqid 
 |-  ran ( x e. B |-> { y e. B | -. y .<_ x } ) = ran ( x e. B |-> { y e. B | -. y .<_ x } )
44 eqid 
 |-  ran ( x e. B |-> { y e. B | -. x .<_ y } ) = ran ( x e. B |-> { y e. B | -. x .<_ y } )
45 1 2 43 44 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 } ) ) ) ) ) )
46 3 45 syl5eq 
 |-  ( 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 } ) ) ) ) ) )
47 42 46 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 )
48 47 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 )
49 28 48 syl 
 |-  ( ( ( 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 )
50 49 unssbd 
 |-  ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> ran ( x e. B |-> { y e. B | -. x .<_ y } ) C_ J )
51 breq2 
 |-  ( z = y -> ( r .<_ z <-> r .<_ y ) )
52 51 notbid 
 |-  ( z = y -> ( -. r .<_ z <-> -. r .<_ y ) )
53 52 cbvrabv 
 |-  { z e. B | -. r .<_ z } = { y e. B | -. r .<_ y }
54 breq1 
 |-  ( x = r -> ( x .<_ y <-> r .<_ y ) )
55 54 notbid 
 |-  ( x = r -> ( -. x .<_ y <-> -. r .<_ y ) )
56 55 rabbidv 
 |-  ( x = r -> { y e. B | -. x .<_ y } = { y e. B | -. r .<_ y } )
57 56 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 } )
58 53 57 mpan2 
 |-  ( r e. B -> E. x e. B { z e. B | -. r .<_ z } = { y e. B | -. x .<_ y } )
59 30 rabex 
 |-  { z e. B | -. r .<_ z } e. _V
60 eqid 
 |-  ( x e. B |-> { y e. B | -. x .<_ y } ) = ( x e. B |-> { y e. B | -. x .<_ y } )
61 60 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 } ) )
62 59 61 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 } )
63 58 62 sylibr 
 |-  ( r e. B -> { z e. B | -. r .<_ z } e. ran ( x e. B |-> { y e. B | -. x .<_ y } ) )
64 63 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 } ) )
65 50 64 sseldd 
 |-  ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> { z e. B | -. r .<_ z } e. J )
66 65 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 )
67 49 unssad 
 |-  ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> ran ( x e. B |-> { y e. B | -. y .<_ x } ) C_ J )
68 breq1 
 |-  ( z = y -> ( z .<_ r <-> y .<_ r ) )
69 68 notbid 
 |-  ( z = y -> ( -. z .<_ r <-> -. y .<_ r ) )
70 69 cbvrabv 
 |-  { z e. B | -. z .<_ r } = { y e. B | -. y .<_ r }
71 breq2 
 |-  ( x = r -> ( y .<_ x <-> y .<_ r ) )
72 71 notbid 
 |-  ( x = r -> ( -. y .<_ x <-> -. y .<_ r ) )
73 72 rabbidv 
 |-  ( x = r -> { y e. B | -. y .<_ x } = { y e. B | -. y .<_ r } )
74 73 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 } )
75 70 74 mpan2 
 |-  ( r e. B -> E. x e. B { z e. B | -. z .<_ r } = { y e. B | -. y .<_ x } )
76 30 rabex 
 |-  { z e. B | -. z .<_ r } e. _V
77 eqid 
 |-  ( x e. B |-> { y e. B | -. y .<_ x } ) = ( x e. B |-> { y e. B | -. y .<_ x } )
78 77 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 } ) )
79 76 78 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 } )
80 75 79 sylibr 
 |-  ( r e. B -> { z e. B | -. z .<_ r } e. ran ( x e. B |-> { y e. B | -. y .<_ x } ) )
81 80 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 } ) )
82 67 81 sseldd 
 |-  ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> { z e. B | -. z .<_ r } e. J )
83 82 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 )
84 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 ) )
85 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 )
86 84 85 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 ) )
87 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 )
88 ssel 
 |-  ( A C_ B -> ( x e. A -> x e. B ) )
89 88 ancrd 
 |-  ( A C_ B -> ( x e. A -> ( x e. B /\ x e. A ) ) )
90 89 anim1d 
 |-  ( A C_ B -> ( ( x e. A /\ -. r .<_ x ) -> ( ( x e. B /\ x e. A ) /\ -. r .<_ x ) ) )
91 90 impl 
 |-  ( ( ( A C_ B /\ x e. A ) /\ -. r .<_ x ) -> ( ( x e. B /\ x e. A ) /\ -. r .<_ x ) )
92 elin 
 |-  ( x e. ( { z e. B | -. r .<_ z } i^i A ) <-> ( x e. { z e. B | -. r .<_ z } /\ x e. A ) )
93 breq2 
 |-  ( z = x -> ( r .<_ z <-> r .<_ x ) )
94 93 notbid 
 |-  ( z = x -> ( -. r .<_ z <-> -. r .<_ x ) )
95 94 elrab 
 |-  ( x e. { z e. B | -. r .<_ z } <-> ( x e. B /\ -. r .<_ x ) )
96 95 anbi1i 
 |-  ( ( x e. { z e. B | -. r .<_ z } /\ x e. A ) <-> ( ( x e. B /\ -. r .<_ x ) /\ x e. A ) )
97 an32 
 |-  ( ( ( x e. B /\ -. r .<_ x ) /\ x e. A ) <-> ( ( x e. B /\ x e. A ) /\ -. r .<_ x ) )
98 92 96 97 3bitri 
 |-  ( x e. ( { z e. B | -. r .<_ z } i^i A ) <-> ( ( x e. B /\ x e. A ) /\ -. r .<_ x ) )
99 91 98 sylibr 
 |-  ( ( ( A C_ B /\ x e. A ) /\ -. r .<_ x ) -> x e. ( { z e. B | -. r .<_ z } i^i A ) )
100 99 ne0d 
 |-  ( ( ( A C_ B /\ x e. A ) /\ -. r .<_ x ) -> ( { z e. B | -. r .<_ z } i^i A ) =/= (/) )
101 25 100 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 ) =/= (/) )
102 101 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 ) =/= (/) )
103 86 87 102 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 ) =/= (/) )
104 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 )
105 ssel 
 |-  ( A C_ B -> ( y e. A -> y e. B ) )
106 105 ancrd 
 |-  ( A C_ B -> ( y e. A -> ( y e. B /\ y e. A ) ) )
107 106 anim1d 
 |-  ( A C_ B -> ( ( y e. A /\ -. y .<_ r ) -> ( ( y e. B /\ y e. A ) /\ -. y .<_ r ) ) )
108 107 impl 
 |-  ( ( ( A C_ B /\ y e. A ) /\ -. y .<_ r ) -> ( ( y e. B /\ y e. A ) /\ -. y .<_ r ) )
109 elin 
 |-  ( y e. ( { z e. B | -. z .<_ r } i^i A ) <-> ( y e. { z e. B | -. z .<_ r } /\ y e. A ) )
110 69 elrab 
 |-  ( y e. { z e. B | -. z .<_ r } <-> ( y e. B /\ -. y .<_ r ) )
111 110 anbi1i 
 |-  ( ( y e. { z e. B | -. z .<_ r } /\ y e. A ) <-> ( ( y e. B /\ -. y .<_ r ) /\ y e. A ) )
112 an32 
 |-  ( ( ( y e. B /\ -. y .<_ r ) /\ y e. A ) <-> ( ( y e. B /\ y e. A ) /\ -. y .<_ r ) )
113 109 111 112 3bitri 
 |-  ( y e. ( { z e. B | -. z .<_ r } i^i A ) <-> ( ( y e. B /\ y e. A ) /\ -. y .<_ r ) )
114 108 113 sylibr 
 |-  ( ( ( A C_ B /\ y e. A ) /\ -. y .<_ r ) -> y e. ( { z e. B | -. z .<_ r } i^i A ) )
115 114 ne0d 
 |-  ( ( ( A C_ B /\ y e. A ) /\ -. y .<_ r ) -> ( { z e. B | -. z .<_ r } i^i A ) =/= (/) )
116 25 115 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 ) =/= (/) )
117 116 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 ) =/= (/) )
118 86 104 117 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 ) =/= (/) )
119 1 2 trleile 
 |-  ( ( K e. Toset /\ r e. B /\ z e. B ) -> ( r .<_ z \/ z .<_ r ) )
120 oran 
 |-  ( ( r .<_ z \/ z .<_ r ) <-> -. ( -. r .<_ z /\ -. z .<_ r ) )
121 119 120 sylib 
 |-  ( ( K e. Toset /\ r e. B /\ z e. B ) -> -. ( -. r .<_ z /\ -. z .<_ r ) )
122 121 3expa 
 |-  ( ( ( K e. Toset /\ r e. B ) /\ z e. B ) -> -. ( -. r .<_ z /\ -. z .<_ r ) )
123 122 nrexdv 
 |-  ( ( K e. Toset /\ r e. B ) -> -. E. z e. B ( -. r .<_ z /\ -. z .<_ r ) )
124 rabid 
 |-  ( z e. { z e. B | -. r .<_ z } <-> ( z e. B /\ -. r .<_ z ) )
125 rabid 
 |-  ( z e. { z e. B | -. z .<_ r } <-> ( z e. B /\ -. z .<_ r ) )
126 124 125 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 ) ) )
127 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 } ) )
128 anandi 
 |-  ( ( z e. B /\ ( -. r .<_ z /\ -. z .<_ r ) ) <-> ( ( z e. B /\ -. r .<_ z ) /\ ( z e. B /\ -. z .<_ r ) ) )
129 126 127 128 3bitr4i 
 |-  ( z e. ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) <-> ( z e. B /\ ( -. r .<_ z /\ -. z .<_ r ) ) )
130 129 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 ) ) )
131 nfrab1 
 |-  F/_ z { z e. B | -. r .<_ z }
132 nfrab1 
 |-  F/_ z { z e. B | -. z .<_ r }
133 131 132 nfin 
 |-  F/_ z ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } )
134 133 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 } ) )
135 df-rex 
 |-  ( E. z e. B ( -. r .<_ z /\ -. z .<_ r ) <-> E. z ( z e. B /\ ( -. r .<_ z /\ -. z .<_ r ) ) )
136 130 134 135 3bitr4i 
 |-  ( ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) =/= (/) <-> E. z e. B ( -. r .<_ z /\ -. z .<_ r ) )
137 136 necon1bbii 
 |-  ( -. E. z e. B ( -. r .<_ z /\ -. z .<_ r ) <-> ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) = (/) )
138 123 137 sylib 
 |-  ( ( K e. Toset /\ r e. B ) -> ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) = (/) )
139 138 adantlr 
 |-  ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) = (/) )
140 139 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 } ) = (/) )
141 140 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 ) )
142 0in 
 |-  ( (/) i^i A ) = (/)
143 141 142 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 ) = (/) )
144 143 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 ) = (/) )
145 simplr 
 |-  ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> r e. B )
146 simpr 
 |-  ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> -. r e. A )
147 vex 
 |-  r e. _V
148 147 snss 
 |-  ( r e. B <-> { r } C_ B )
149 eldif 
 |-  ( r e. ( B \ A ) <-> ( r e. B /\ -. r e. A ) )
150 147 snss 
 |-  ( r e. ( B \ A ) <-> { r } C_ ( B \ A ) )
151 149 150 bitr3i 
 |-  ( ( r e. B /\ -. r e. A ) <-> { r } C_ ( B \ A ) )
152 ssconb 
 |-  ( ( { r } C_ B /\ A C_ B ) -> ( { r } C_ ( B \ A ) <-> A C_ ( B \ { r } ) ) )
153 151 152 syl5bb 
 |-  ( ( { r } C_ B /\ A C_ B ) -> ( ( r e. B /\ -. r e. A ) <-> A C_ ( B \ { r } ) ) )
154 148 153 sylanb 
 |-  ( ( r e. B /\ A C_ B ) -> ( ( r e. B /\ -. r e. A ) <-> A C_ ( B \ { r } ) ) )
155 154 adantl 
 |-  ( ( K e. Toset /\ ( r e. B /\ A C_ B ) ) -> ( ( r e. B /\ -. r e. A ) <-> A C_ ( B \ { r } ) ) )
156 155 anass1rs 
 |-  ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> ( ( r e. B /\ -. r e. A ) <-> A C_ ( B \ { r } ) ) )
157 156 adantr 
 |-  ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> ( ( r e. B /\ -. r e. A ) <-> A C_ ( B \ { r } ) ) )
158 145 146 157 mpbi2and 
 |-  ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> A C_ ( B \ { r } ) )
159 10 ad3antrrr 
 |-  ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> K e. Poset )
160 nfv 
 |-  F/ z ( K e. Poset /\ r e. B )
161 131 132 nfun 
 |-  F/_ z ( { z e. B | -. r .<_ z } u. { z e. B | -. z .<_ r } )
162 nfcv 
 |-  F/_ z ( B \ { r } )
163 ianor 
 |-  ( -. ( r .<_ z /\ z .<_ r ) <-> ( -. r .<_ z \/ -. z .<_ r ) )
164 1 2 posrasymb 
 |-  ( ( K e. Poset /\ r e. B /\ z e. B ) -> ( ( r .<_ z /\ z .<_ r ) <-> r = z ) )
165 equcom 
 |-  ( r = z <-> z = r )
166 164 165 syl6bb 
 |-  ( ( K e. Poset /\ r e. B /\ z e. B ) -> ( ( r .<_ z /\ z .<_ r ) <-> z = r ) )
167 166 necon3bbid 
 |-  ( ( K e. Poset /\ r e. B /\ z e. B ) -> ( -. ( r .<_ z /\ z .<_ r ) <-> z =/= r ) )
168 163 167 bitr3id 
 |-  ( ( K e. Poset /\ r e. B /\ z e. B ) -> ( ( -. r .<_ z \/ -. z .<_ r ) <-> z =/= r ) )
169 168 3expia 
 |-  ( ( K e. Poset /\ r e. B ) -> ( z e. B -> ( ( -. r .<_ z \/ -. z .<_ r ) <-> z =/= r ) ) )
170 169 pm5.32d 
 |-  ( ( K e. Poset /\ r e. B ) -> ( ( z e. B /\ ( -. r .<_ z \/ -. z .<_ r ) ) <-> ( z e. B /\ z =/= r ) ) )
171 124 125 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 ) ) )
172 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 } ) )
173 andi 
 |-  ( ( z e. B /\ ( -. r .<_ z \/ -. z .<_ r ) ) <-> ( ( z e. B /\ -. r .<_ z ) \/ ( z e. B /\ -. z .<_ r ) ) )
174 171 172 173 3bitr4ri 
 |-  ( ( z e. B /\ ( -. r .<_ z \/ -. z .<_ r ) ) <-> z e. ( { z e. B | -. r .<_ z } u. { z e. B | -. z .<_ r } ) )
175 eldifsn 
 |-  ( z e. ( B \ { r } ) <-> ( z e. B /\ z =/= r ) )
176 175 bicomi 
 |-  ( ( z e. B /\ z =/= r ) <-> z e. ( B \ { r } ) )
177 170 174 176 3bitr3g 
 |-  ( ( K e. Poset /\ r e. B ) -> ( z e. ( { z e. B | -. r .<_ z } u. { z e. B | -. z .<_ r } ) <-> z e. ( B \ { r } ) ) )
178 160 161 162 177 eqrd 
 |-  ( ( K e. Poset /\ r e. B ) -> ( { z e. B | -. r .<_ z } u. { z e. B | -. z .<_ r } ) = ( B \ { r } ) )
179 159 145 178 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 } ) )
180 158 179 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 } ) )
181 180 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 } ) )
182 24 26 66 83 103 118 144 181 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 )
183 182 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 )
184 183 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 )
185 rexanali 
 |-  ( E. r e. B ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> -. A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) )
186 185 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 ) )
187 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 ) )
188 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 ) )
189 186 187 188 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 ) )
190 189 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 ) )
191 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 ) )
192 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 ) )
193 190 191 192 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 ) )
194 r19.41v 
 |-  ( E. y e. A ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> ( E. y e. A ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) )
195 194 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 ) )
196 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 ) )
197 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 ) )
198 197 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 ) )
199 195 196 198 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 ) )
200 199 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 ) )
201 193 200 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 ) )
202 27 ad2antrr 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> K e. Toset )
203 25 sselda 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> x e. B )
204 simpllr 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> r e. B )
205 1 2 trleile 
 |-  ( ( K e. Toset /\ x e. B /\ r e. B ) -> ( x .<_ r \/ r .<_ x ) )
206 202 203 204 205 syl3anc 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> ( x .<_ r \/ r .<_ x ) )
207 simpr 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> x e. A )
208 simplr 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> -. r e. A )
209 nelne2 
 |-  ( ( x e. A /\ -. r e. A ) -> x =/= r )
210 207 208 209 syl2anc 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> x =/= r )
211 159 adantr 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> K e. Poset )
212 1 2 posrasymb 
 |-  ( ( K e. Poset /\ x e. B /\ r e. B ) -> ( ( x .<_ r /\ r .<_ x ) <-> x = r ) )
213 212 necon3bbid 
 |-  ( ( K e. Poset /\ x e. B /\ r e. B ) -> ( -. ( x .<_ r /\ r .<_ x ) <-> x =/= r ) )
214 211 203 204 213 syl3anc 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> ( -. ( x .<_ r /\ r .<_ x ) <-> x =/= r ) )
215 210 214 mpbird 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> -. ( x .<_ r /\ r .<_ x ) )
216 206 215 jca 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> ( ( x .<_ r \/ r .<_ x ) /\ -. ( x .<_ r /\ r .<_ x ) ) )
217 pm5.17 
 |-  ( ( ( x .<_ r \/ r .<_ x ) /\ -. ( x .<_ r /\ r .<_ x ) ) <-> ( x .<_ r <-> -. r .<_ x ) )
218 216 217 sylib 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> ( x .<_ r <-> -. r .<_ x ) )
219 218 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 ) )
220 27 ad2antrr 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> K e. Toset )
221 simpllr 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> r e. B )
222 25 sselda 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> y e. B )
223 1 2 trleile 
 |-  ( ( K e. Toset /\ r e. B /\ y e. B ) -> ( r .<_ y \/ y .<_ r ) )
224 220 221 222 223 syl3anc 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> ( r .<_ y \/ y .<_ r ) )
225 simpr 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> y e. A )
226 simplr 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> -. r e. A )
227 nelne2 
 |-  ( ( y e. A /\ -. r e. A ) -> y =/= r )
228 225 226 227 syl2anc 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> y =/= r )
229 228 necomd 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> r =/= y )
230 159 adantr 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> K e. Poset )
231 1 2 posrasymb 
 |-  ( ( K e. Poset /\ r e. B /\ y e. B ) -> ( ( r .<_ y /\ y .<_ r ) <-> r = y ) )
232 231 necon3bbid 
 |-  ( ( K e. Poset /\ r e. B /\ y e. B ) -> ( -. ( r .<_ y /\ y .<_ r ) <-> r =/= y ) )
233 230 221 222 232 syl3anc 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> ( -. ( r .<_ y /\ y .<_ r ) <-> r =/= y ) )
234 229 233 mpbird 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> -. ( r .<_ y /\ y .<_ r ) )
235 224 234 jca 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> ( ( r .<_ y \/ y .<_ r ) /\ -. ( r .<_ y /\ y .<_ r ) ) )
236 pm5.17 
 |-  ( ( ( r .<_ y \/ y .<_ r ) /\ -. ( r .<_ y /\ y .<_ r ) ) <-> ( r .<_ y <-> -. y .<_ r ) )
237 235 236 sylib 
 |-  ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> ( r .<_ y <-> -. y .<_ r ) )
238 237 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 ) )
239 219 238 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 ) ) )
240 239 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 ) ) ) )
241 240 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 ) ) )
242 241 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 ) ) )
243 201 242 syl5bb 
 |-  ( ( 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 243 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 ) )
245 9 184 244 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 )
246 245 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 ) )
247 246 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 ) ) )