Step |
Hyp |
Ref |
Expression |
1 |
|
funmpt |
|- Fun ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) |
2 |
|
funiunfv |
|- ( Fun ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) -> U_ c e. ( ~P a i^i Fin ) ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) ` c ) = U. ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) " ( ~P a i^i Fin ) ) ) |
3 |
1 2
|
mp1i |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> U_ c e. ( ~P a i^i Fin ) ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) ` c ) = U. ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) " ( ~P a i^i Fin ) ) ) |
4 |
|
elinel1 |
|- ( c e. ( ~P a i^i Fin ) -> c e. ~P a ) |
5 |
4
|
elpwid |
|- ( c e. ( ~P a i^i Fin ) -> c C_ a ) |
6 |
|
elpwi |
|- ( a e. ~P X -> a C_ X ) |
7 |
5 6
|
sylan9ssr |
|- ( ( a e. ~P X /\ c e. ( ~P a i^i Fin ) ) -> c C_ X ) |
8 |
|
velpw |
|- ( c e. ~P X <-> c C_ X ) |
9 |
7 8
|
sylibr |
|- ( ( a e. ~P X /\ c e. ( ~P a i^i Fin ) ) -> c e. ~P X ) |
10 |
9
|
adantll |
|- ( ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) /\ c e. ( ~P a i^i Fin ) ) -> c e. ~P X ) |
11 |
|
eqeq1 |
|- ( b = c -> ( b = T <-> c = T ) ) |
12 |
11
|
ifbid |
|- ( b = c -> if ( b = T , { K } , (/) ) = if ( c = T , { K } , (/) ) ) |
13 |
|
eqid |
|- ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) = ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) |
14 |
|
snex |
|- { K } e. _V |
15 |
|
0ex |
|- (/) e. _V |
16 |
14 15
|
ifex |
|- if ( c = T , { K } , (/) ) e. _V |
17 |
12 13 16
|
fvmpt |
|- ( c e. ~P X -> ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) ` c ) = if ( c = T , { K } , (/) ) ) |
18 |
10 17
|
syl |
|- ( ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) /\ c e. ( ~P a i^i Fin ) ) -> ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) ` c ) = if ( c = T , { K } , (/) ) ) |
19 |
18
|
iuneq2dv |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> U_ c e. ( ~P a i^i Fin ) ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) ` c ) = U_ c e. ( ~P a i^i Fin ) if ( c = T , { K } , (/) ) ) |
20 |
3 19
|
eqtr3d |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> U. ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) " ( ~P a i^i Fin ) ) = U_ c e. ( ~P a i^i Fin ) if ( c = T , { K } , (/) ) ) |
21 |
20
|
sseq1d |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( U. ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) " ( ~P a i^i Fin ) ) C_ a <-> U_ c e. ( ~P a i^i Fin ) if ( c = T , { K } , (/) ) C_ a ) ) |
22 |
|
iunss |
|- ( U_ c e. ( ~P a i^i Fin ) if ( c = T , { K } , (/) ) C_ a <-> A. c e. ( ~P a i^i Fin ) if ( c = T , { K } , (/) ) C_ a ) |
23 |
|
sseq1 |
|- ( { K } = if ( c = T , { K } , (/) ) -> ( { K } C_ a <-> if ( c = T , { K } , (/) ) C_ a ) ) |
24 |
23
|
bibi1d |
|- ( { K } = if ( c = T , { K } , (/) ) -> ( ( { K } C_ a <-> ( c = T -> K e. a ) ) <-> ( if ( c = T , { K } , (/) ) C_ a <-> ( c = T -> K e. a ) ) ) ) |
25 |
|
sseq1 |
|- ( (/) = if ( c = T , { K } , (/) ) -> ( (/) C_ a <-> if ( c = T , { K } , (/) ) C_ a ) ) |
26 |
25
|
bibi1d |
|- ( (/) = if ( c = T , { K } , (/) ) -> ( ( (/) C_ a <-> ( c = T -> K e. a ) ) <-> ( if ( c = T , { K } , (/) ) C_ a <-> ( c = T -> K e. a ) ) ) ) |
27 |
|
snssg |
|- ( K e. X -> ( K e. a <-> { K } C_ a ) ) |
28 |
27
|
adantr |
|- ( ( K e. X /\ c = T ) -> ( K e. a <-> { K } C_ a ) ) |
29 |
|
biimt |
|- ( c = T -> ( K e. a <-> ( c = T -> K e. a ) ) ) |
30 |
29
|
adantl |
|- ( ( K e. X /\ c = T ) -> ( K e. a <-> ( c = T -> K e. a ) ) ) |
31 |
28 30
|
bitr3d |
|- ( ( K e. X /\ c = T ) -> ( { K } C_ a <-> ( c = T -> K e. a ) ) ) |
32 |
|
0ss |
|- (/) C_ a |
33 |
32
|
a1i |
|- ( -. c = T -> (/) C_ a ) |
34 |
|
pm2.21 |
|- ( -. c = T -> ( c = T -> K e. a ) ) |
35 |
33 34
|
2thd |
|- ( -. c = T -> ( (/) C_ a <-> ( c = T -> K e. a ) ) ) |
36 |
35
|
adantl |
|- ( ( K e. X /\ -. c = T ) -> ( (/) C_ a <-> ( c = T -> K e. a ) ) ) |
37 |
24 26 31 36
|
ifbothda |
|- ( K e. X -> ( if ( c = T , { K } , (/) ) C_ a <-> ( c = T -> K e. a ) ) ) |
38 |
37
|
ralbidv |
|- ( K e. X -> ( A. c e. ( ~P a i^i Fin ) if ( c = T , { K } , (/) ) C_ a <-> A. c e. ( ~P a i^i Fin ) ( c = T -> K e. a ) ) ) |
39 |
38
|
ad3antlr |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( A. c e. ( ~P a i^i Fin ) if ( c = T , { K } , (/) ) C_ a <-> A. c e. ( ~P a i^i Fin ) ( c = T -> K e. a ) ) ) |
40 |
22 39
|
syl5bb |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( U_ c e. ( ~P a i^i Fin ) if ( c = T , { K } , (/) ) C_ a <-> A. c e. ( ~P a i^i Fin ) ( c = T -> K e. a ) ) ) |
41 |
|
inss1 |
|- ( ~P a i^i Fin ) C_ ~P a |
42 |
6
|
sspwd |
|- ( a e. ~P X -> ~P a C_ ~P X ) |
43 |
41 42
|
sstrid |
|- ( a e. ~P X -> ( ~P a i^i Fin ) C_ ~P X ) |
44 |
43
|
adantl |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( ~P a i^i Fin ) C_ ~P X ) |
45 |
|
ralss |
|- ( ( ~P a i^i Fin ) C_ ~P X -> ( A. c e. ( ~P a i^i Fin ) ( c = T -> K e. a ) <-> A. c e. ~P X ( c e. ( ~P a i^i Fin ) -> ( c = T -> K e. a ) ) ) ) |
46 |
44 45
|
syl |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( A. c e. ( ~P a i^i Fin ) ( c = T -> K e. a ) <-> A. c e. ~P X ( c e. ( ~P a i^i Fin ) -> ( c = T -> K e. a ) ) ) ) |
47 |
|
bi2.04 |
|- ( ( c e. ( ~P a i^i Fin ) -> ( c = T -> K e. a ) ) <-> ( c = T -> ( c e. ( ~P a i^i Fin ) -> K e. a ) ) ) |
48 |
47
|
ralbii |
|- ( A. c e. ~P X ( c e. ( ~P a i^i Fin ) -> ( c = T -> K e. a ) ) <-> A. c e. ~P X ( c = T -> ( c e. ( ~P a i^i Fin ) -> K e. a ) ) ) |
49 |
|
elpwg |
|- ( T e. Fin -> ( T e. ~P X <-> T C_ X ) ) |
50 |
49
|
biimparc |
|- ( ( T C_ X /\ T e. Fin ) -> T e. ~P X ) |
51 |
50
|
ad2antlr |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> T e. ~P X ) |
52 |
|
eleq1 |
|- ( c = T -> ( c e. ( ~P a i^i Fin ) <-> T e. ( ~P a i^i Fin ) ) ) |
53 |
52
|
imbi1d |
|- ( c = T -> ( ( c e. ( ~P a i^i Fin ) -> K e. a ) <-> ( T e. ( ~P a i^i Fin ) -> K e. a ) ) ) |
54 |
53
|
ceqsralv |
|- ( T e. ~P X -> ( A. c e. ~P X ( c = T -> ( c e. ( ~P a i^i Fin ) -> K e. a ) ) <-> ( T e. ( ~P a i^i Fin ) -> K e. a ) ) ) |
55 |
51 54
|
syl |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( A. c e. ~P X ( c = T -> ( c e. ( ~P a i^i Fin ) -> K e. a ) ) <-> ( T e. ( ~P a i^i Fin ) -> K e. a ) ) ) |
56 |
48 55
|
syl5bb |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( A. c e. ~P X ( c e. ( ~P a i^i Fin ) -> ( c = T -> K e. a ) ) <-> ( T e. ( ~P a i^i Fin ) -> K e. a ) ) ) |
57 |
|
simplrr |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> T e. Fin ) |
58 |
57
|
biantrud |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( T e. ~P a <-> ( T e. ~P a /\ T e. Fin ) ) ) |
59 |
|
elin |
|- ( T e. ( ~P a i^i Fin ) <-> ( T e. ~P a /\ T e. Fin ) ) |
60 |
58 59
|
bitr4di |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( T e. ~P a <-> T e. ( ~P a i^i Fin ) ) ) |
61 |
|
vex |
|- a e. _V |
62 |
61
|
elpw2 |
|- ( T e. ~P a <-> T C_ a ) |
63 |
60 62
|
bitr3di |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( T e. ( ~P a i^i Fin ) <-> T C_ a ) ) |
64 |
63
|
imbi1d |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( ( T e. ( ~P a i^i Fin ) -> K e. a ) <-> ( T C_ a -> K e. a ) ) ) |
65 |
46 56 64
|
3bitrd |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( A. c e. ( ~P a i^i Fin ) ( c = T -> K e. a ) <-> ( T C_ a -> K e. a ) ) ) |
66 |
21 40 65
|
3bitrrd |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ a e. ~P X ) -> ( ( T C_ a -> K e. a ) <-> U. ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) " ( ~P a i^i Fin ) ) C_ a ) ) |
67 |
66
|
rabbidva |
|- ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) -> { a e. ~P X | ( T C_ a -> K e. a ) } = { a e. ~P X | U. ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) " ( ~P a i^i Fin ) ) C_ a } ) |
68 |
|
simpll |
|- ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) -> X e. V ) |
69 |
|
snelpwi |
|- ( K e. X -> { K } e. ~P X ) |
70 |
69
|
ad2antlr |
|- ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) -> { K } e. ~P X ) |
71 |
|
0elpw |
|- (/) e. ~P X |
72 |
|
ifcl |
|- ( ( { K } e. ~P X /\ (/) e. ~P X ) -> if ( b = T , { K } , (/) ) e. ~P X ) |
73 |
70 71 72
|
sylancl |
|- ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) -> if ( b = T , { K } , (/) ) e. ~P X ) |
74 |
73
|
adantr |
|- ( ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) /\ b e. ~P X ) -> if ( b = T , { K } , (/) ) e. ~P X ) |
75 |
74
|
fmpttd |
|- ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) -> ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) : ~P X --> ~P X ) |
76 |
|
isacs1i |
|- ( ( X e. V /\ ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) : ~P X --> ~P X ) -> { a e. ~P X | U. ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) " ( ~P a i^i Fin ) ) C_ a } e. ( ACS ` X ) ) |
77 |
68 75 76
|
syl2anc |
|- ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) -> { a e. ~P X | U. ( ( b e. ~P X |-> if ( b = T , { K } , (/) ) ) " ( ~P a i^i Fin ) ) C_ a } e. ( ACS ` X ) ) |
78 |
67 77
|
eqeltrd |
|- ( ( ( X e. V /\ K e. X ) /\ ( T C_ X /\ T e. Fin ) ) -> { a e. ~P X | ( T C_ a -> K e. a ) } e. ( ACS ` X ) ) |