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 ) ) ) |