Step |
Hyp |
Ref |
Expression |
1 |
|
tsmsfbas.s |
|- S = ( ~P A i^i Fin ) |
2 |
|
tsmsfbas.f |
|- F = ( z e. S |-> { y e. S | z C_ y } ) |
3 |
|
tsmsfbas.l |
|- L = ran F |
4 |
|
tsmsfbas.a |
|- ( ph -> A e. W ) |
5 |
|
elex |
|- ( A e. W -> A e. _V ) |
6 |
|
ssrab2 |
|- { y e. S | z C_ y } C_ S |
7 |
|
pwexg |
|- ( A e. _V -> ~P A e. _V ) |
8 |
|
inex1g |
|- ( ~P A e. _V -> ( ~P A i^i Fin ) e. _V ) |
9 |
7 8
|
syl |
|- ( A e. _V -> ( ~P A i^i Fin ) e. _V ) |
10 |
1 9
|
eqeltrid |
|- ( A e. _V -> S e. _V ) |
11 |
10
|
adantr |
|- ( ( A e. _V /\ z e. S ) -> S e. _V ) |
12 |
|
elpw2g |
|- ( S e. _V -> ( { y e. S | z C_ y } e. ~P S <-> { y e. S | z C_ y } C_ S ) ) |
13 |
11 12
|
syl |
|- ( ( A e. _V /\ z e. S ) -> ( { y e. S | z C_ y } e. ~P S <-> { y e. S | z C_ y } C_ S ) ) |
14 |
6 13
|
mpbiri |
|- ( ( A e. _V /\ z e. S ) -> { y e. S | z C_ y } e. ~P S ) |
15 |
14 2
|
fmptd |
|- ( A e. _V -> F : S --> ~P S ) |
16 |
15
|
frnd |
|- ( A e. _V -> ran F C_ ~P S ) |
17 |
|
0ss |
|- (/) C_ A |
18 |
|
0fin |
|- (/) e. Fin |
19 |
|
elfpw |
|- ( (/) e. ( ~P A i^i Fin ) <-> ( (/) C_ A /\ (/) e. Fin ) ) |
20 |
17 18 19
|
mpbir2an |
|- (/) e. ( ~P A i^i Fin ) |
21 |
20 1
|
eleqtrri |
|- (/) e. S |
22 |
|
0ss |
|- (/) C_ y |
23 |
22
|
rgenw |
|- A. y e. S (/) C_ y |
24 |
|
rabid2 |
|- ( S = { y e. S | z C_ y } <-> A. y e. S z C_ y ) |
25 |
|
sseq1 |
|- ( z = (/) -> ( z C_ y <-> (/) C_ y ) ) |
26 |
25
|
ralbidv |
|- ( z = (/) -> ( A. y e. S z C_ y <-> A. y e. S (/) C_ y ) ) |
27 |
24 26
|
syl5bb |
|- ( z = (/) -> ( S = { y e. S | z C_ y } <-> A. y e. S (/) C_ y ) ) |
28 |
27
|
rspcev |
|- ( ( (/) e. S /\ A. y e. S (/) C_ y ) -> E. z e. S S = { y e. S | z C_ y } ) |
29 |
21 23 28
|
mp2an |
|- E. z e. S S = { y e. S | z C_ y } |
30 |
2
|
elrnmpt |
|- ( S e. _V -> ( S e. ran F <-> E. z e. S S = { y e. S | z C_ y } ) ) |
31 |
10 30
|
syl |
|- ( A e. _V -> ( S e. ran F <-> E. z e. S S = { y e. S | z C_ y } ) ) |
32 |
29 31
|
mpbiri |
|- ( A e. _V -> S e. ran F ) |
33 |
32
|
ne0d |
|- ( A e. _V -> ran F =/= (/) ) |
34 |
|
simpr |
|- ( ( A e. _V /\ z e. S ) -> z e. S ) |
35 |
|
ssid |
|- z C_ z |
36 |
|
sseq2 |
|- ( y = z -> ( z C_ y <-> z C_ z ) ) |
37 |
36
|
rspcev |
|- ( ( z e. S /\ z C_ z ) -> E. y e. S z C_ y ) |
38 |
34 35 37
|
sylancl |
|- ( ( A e. _V /\ z e. S ) -> E. y e. S z C_ y ) |
39 |
|
rabn0 |
|- ( { y e. S | z C_ y } =/= (/) <-> E. y e. S z C_ y ) |
40 |
38 39
|
sylibr |
|- ( ( A e. _V /\ z e. S ) -> { y e. S | z C_ y } =/= (/) ) |
41 |
40
|
necomd |
|- ( ( A e. _V /\ z e. S ) -> (/) =/= { y e. S | z C_ y } ) |
42 |
41
|
neneqd |
|- ( ( A e. _V /\ z e. S ) -> -. (/) = { y e. S | z C_ y } ) |
43 |
42
|
nrexdv |
|- ( A e. _V -> -. E. z e. S (/) = { y e. S | z C_ y } ) |
44 |
|
0ex |
|- (/) e. _V |
45 |
2
|
elrnmpt |
|- ( (/) e. _V -> ( (/) e. ran F <-> E. z e. S (/) = { y e. S | z C_ y } ) ) |
46 |
44 45
|
ax-mp |
|- ( (/) e. ran F <-> E. z e. S (/) = { y e. S | z C_ y } ) |
47 |
43 46
|
sylnibr |
|- ( A e. _V -> -. (/) e. ran F ) |
48 |
|
df-nel |
|- ( (/) e/ ran F <-> -. (/) e. ran F ) |
49 |
47 48
|
sylibr |
|- ( A e. _V -> (/) e/ ran F ) |
50 |
|
elfpw |
|- ( u e. ( ~P A i^i Fin ) <-> ( u C_ A /\ u e. Fin ) ) |
51 |
50
|
simplbi |
|- ( u e. ( ~P A i^i Fin ) -> u C_ A ) |
52 |
51 1
|
eleq2s |
|- ( u e. S -> u C_ A ) |
53 |
|
elfpw |
|- ( v e. ( ~P A i^i Fin ) <-> ( v C_ A /\ v e. Fin ) ) |
54 |
53
|
simplbi |
|- ( v e. ( ~P A i^i Fin ) -> v C_ A ) |
55 |
54 1
|
eleq2s |
|- ( v e. S -> v C_ A ) |
56 |
52 55
|
anim12i |
|- ( ( u e. S /\ v e. S ) -> ( u C_ A /\ v C_ A ) ) |
57 |
|
unss |
|- ( ( u C_ A /\ v C_ A ) <-> ( u u. v ) C_ A ) |
58 |
56 57
|
sylib |
|- ( ( u e. S /\ v e. S ) -> ( u u. v ) C_ A ) |
59 |
|
elinel2 |
|- ( u e. ( ~P A i^i Fin ) -> u e. Fin ) |
60 |
59 1
|
eleq2s |
|- ( u e. S -> u e. Fin ) |
61 |
|
elinel2 |
|- ( v e. ( ~P A i^i Fin ) -> v e. Fin ) |
62 |
61 1
|
eleq2s |
|- ( v e. S -> v e. Fin ) |
63 |
|
unfi |
|- ( ( u e. Fin /\ v e. Fin ) -> ( u u. v ) e. Fin ) |
64 |
60 62 63
|
syl2an |
|- ( ( u e. S /\ v e. S ) -> ( u u. v ) e. Fin ) |
65 |
|
elfpw |
|- ( ( u u. v ) e. ( ~P A i^i Fin ) <-> ( ( u u. v ) C_ A /\ ( u u. v ) e. Fin ) ) |
66 |
58 64 65
|
sylanbrc |
|- ( ( u e. S /\ v e. S ) -> ( u u. v ) e. ( ~P A i^i Fin ) ) |
67 |
66
|
adantl |
|- ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> ( u u. v ) e. ( ~P A i^i Fin ) ) |
68 |
67 1
|
eleqtrrdi |
|- ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> ( u u. v ) e. S ) |
69 |
|
eqidd |
|- ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> { y e. S | ( u u. v ) C_ y } = { y e. S | ( u u. v ) C_ y } ) |
70 |
|
sseq1 |
|- ( a = ( u u. v ) -> ( a C_ y <-> ( u u. v ) C_ y ) ) |
71 |
70
|
rabbidv |
|- ( a = ( u u. v ) -> { y e. S | a C_ y } = { y e. S | ( u u. v ) C_ y } ) |
72 |
71
|
rspceeqv |
|- ( ( ( u u. v ) e. S /\ { y e. S | ( u u. v ) C_ y } = { y e. S | ( u u. v ) C_ y } ) -> E. a e. S { y e. S | ( u u. v ) C_ y } = { y e. S | a C_ y } ) |
73 |
68 69 72
|
syl2anc |
|- ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> E. a e. S { y e. S | ( u u. v ) C_ y } = { y e. S | a C_ y } ) |
74 |
10
|
adantr |
|- ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> S e. _V ) |
75 |
|
rabexg |
|- ( S e. _V -> { y e. S | ( u u. v ) C_ y } e. _V ) |
76 |
74 75
|
syl |
|- ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> { y e. S | ( u u. v ) C_ y } e. _V ) |
77 |
|
sseq1 |
|- ( z = a -> ( z C_ y <-> a C_ y ) ) |
78 |
77
|
rabbidv |
|- ( z = a -> { y e. S | z C_ y } = { y e. S | a C_ y } ) |
79 |
78
|
cbvmptv |
|- ( z e. S |-> { y e. S | z C_ y } ) = ( a e. S |-> { y e. S | a C_ y } ) |
80 |
2 79
|
eqtri |
|- F = ( a e. S |-> { y e. S | a C_ y } ) |
81 |
80
|
elrnmpt |
|- ( { y e. S | ( u u. v ) C_ y } e. _V -> ( { y e. S | ( u u. v ) C_ y } e. ran F <-> E. a e. S { y e. S | ( u u. v ) C_ y } = { y e. S | a C_ y } ) ) |
82 |
76 81
|
syl |
|- ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> ( { y e. S | ( u u. v ) C_ y } e. ran F <-> E. a e. S { y e. S | ( u u. v ) C_ y } = { y e. S | a C_ y } ) ) |
83 |
73 82
|
mpbird |
|- ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> { y e. S | ( u u. v ) C_ y } e. ran F ) |
84 |
|
pwidg |
|- ( { y e. S | ( u u. v ) C_ y } e. _V -> { y e. S | ( u u. v ) C_ y } e. ~P { y e. S | ( u u. v ) C_ y } ) |
85 |
76 84
|
syl |
|- ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> { y e. S | ( u u. v ) C_ y } e. ~P { y e. S | ( u u. v ) C_ y } ) |
86 |
|
inelcm |
|- ( ( { y e. S | ( u u. v ) C_ y } e. ran F /\ { y e. S | ( u u. v ) C_ y } e. ~P { y e. S | ( u u. v ) C_ y } ) -> ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) ) |
87 |
83 85 86
|
syl2anc |
|- ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) ) |
88 |
87
|
ralrimivva |
|- ( A e. _V -> A. u e. S A. v e. S ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) ) |
89 |
|
rabexg |
|- ( S e. _V -> { y e. S | u C_ y } e. _V ) |
90 |
10 89
|
syl |
|- ( A e. _V -> { y e. S | u C_ y } e. _V ) |
91 |
90
|
ralrimivw |
|- ( A e. _V -> A. u e. S { y e. S | u C_ y } e. _V ) |
92 |
|
sseq1 |
|- ( z = u -> ( z C_ y <-> u C_ y ) ) |
93 |
92
|
rabbidv |
|- ( z = u -> { y e. S | z C_ y } = { y e. S | u C_ y } ) |
94 |
93
|
cbvmptv |
|- ( z e. S |-> { y e. S | z C_ y } ) = ( u e. S |-> { y e. S | u C_ y } ) |
95 |
2 94
|
eqtri |
|- F = ( u e. S |-> { y e. S | u C_ y } ) |
96 |
|
ineq1 |
|- ( a = { y e. S | u C_ y } -> ( a i^i { y e. S | v C_ y } ) = ( { y e. S | u C_ y } i^i { y e. S | v C_ y } ) ) |
97 |
|
inrab |
|- ( { y e. S | u C_ y } i^i { y e. S | v C_ y } ) = { y e. S | ( u C_ y /\ v C_ y ) } |
98 |
|
unss |
|- ( ( u C_ y /\ v C_ y ) <-> ( u u. v ) C_ y ) |
99 |
98
|
rabbii |
|- { y e. S | ( u C_ y /\ v C_ y ) } = { y e. S | ( u u. v ) C_ y } |
100 |
97 99
|
eqtri |
|- ( { y e. S | u C_ y } i^i { y e. S | v C_ y } ) = { y e. S | ( u u. v ) C_ y } |
101 |
96 100
|
eqtrdi |
|- ( a = { y e. S | u C_ y } -> ( a i^i { y e. S | v C_ y } ) = { y e. S | ( u u. v ) C_ y } ) |
102 |
101
|
pweqd |
|- ( a = { y e. S | u C_ y } -> ~P ( a i^i { y e. S | v C_ y } ) = ~P { y e. S | ( u u. v ) C_ y } ) |
103 |
102
|
ineq2d |
|- ( a = { y e. S | u C_ y } -> ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) = ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) ) |
104 |
103
|
neeq1d |
|- ( a = { y e. S | u C_ y } -> ( ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) <-> ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) ) ) |
105 |
104
|
ralbidv |
|- ( a = { y e. S | u C_ y } -> ( A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) <-> A. v e. S ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) ) ) |
106 |
95 105
|
ralrnmptw |
|- ( A. u e. S { y e. S | u C_ y } e. _V -> ( A. a e. ran F A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) <-> A. u e. S A. v e. S ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) ) ) |
107 |
91 106
|
syl |
|- ( A e. _V -> ( A. a e. ran F A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) <-> A. u e. S A. v e. S ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) ) ) |
108 |
88 107
|
mpbird |
|- ( A e. _V -> A. a e. ran F A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) ) |
109 |
|
rabexg |
|- ( S e. _V -> { y e. S | v C_ y } e. _V ) |
110 |
10 109
|
syl |
|- ( A e. _V -> { y e. S | v C_ y } e. _V ) |
111 |
110
|
ralrimivw |
|- ( A e. _V -> A. v e. S { y e. S | v C_ y } e. _V ) |
112 |
|
sseq1 |
|- ( z = v -> ( z C_ y <-> v C_ y ) ) |
113 |
112
|
rabbidv |
|- ( z = v -> { y e. S | z C_ y } = { y e. S | v C_ y } ) |
114 |
113
|
cbvmptv |
|- ( z e. S |-> { y e. S | z C_ y } ) = ( v e. S |-> { y e. S | v C_ y } ) |
115 |
2 114
|
eqtri |
|- F = ( v e. S |-> { y e. S | v C_ y } ) |
116 |
|
ineq2 |
|- ( b = { y e. S | v C_ y } -> ( a i^i b ) = ( a i^i { y e. S | v C_ y } ) ) |
117 |
116
|
pweqd |
|- ( b = { y e. S | v C_ y } -> ~P ( a i^i b ) = ~P ( a i^i { y e. S | v C_ y } ) ) |
118 |
117
|
ineq2d |
|- ( b = { y e. S | v C_ y } -> ( ran F i^i ~P ( a i^i b ) ) = ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) ) |
119 |
118
|
neeq1d |
|- ( b = { y e. S | v C_ y } -> ( ( ran F i^i ~P ( a i^i b ) ) =/= (/) <-> ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) ) ) |
120 |
115 119
|
ralrnmptw |
|- ( A. v e. S { y e. S | v C_ y } e. _V -> ( A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) <-> A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) ) ) |
121 |
111 120
|
syl |
|- ( A e. _V -> ( A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) <-> A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) ) ) |
122 |
121
|
ralbidv |
|- ( A e. _V -> ( A. a e. ran F A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) <-> A. a e. ran F A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) ) ) |
123 |
108 122
|
mpbird |
|- ( A e. _V -> A. a e. ran F A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) ) |
124 |
33 49 123
|
3jca |
|- ( A e. _V -> ( ran F =/= (/) /\ (/) e/ ran F /\ A. a e. ran F A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) ) ) |
125 |
|
isfbas |
|- ( S e. _V -> ( ran F e. ( fBas ` S ) <-> ( ran F C_ ~P S /\ ( ran F =/= (/) /\ (/) e/ ran F /\ A. a e. ran F A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) ) ) ) ) |
126 |
10 125
|
syl |
|- ( A e. _V -> ( ran F e. ( fBas ` S ) <-> ( ran F C_ ~P S /\ ( ran F =/= (/) /\ (/) e/ ran F /\ A. a e. ran F A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) ) ) ) ) |
127 |
16 124 126
|
mpbir2and |
|- ( A e. _V -> ran F e. ( fBas ` S ) ) |
128 |
3 127
|
eqeltrid |
|- ( A e. _V -> L e. ( fBas ` S ) ) |
129 |
4 5 128
|
3syl |
|- ( ph -> L e. ( fBas ` S ) ) |