Step |
Hyp |
Ref |
Expression |
1 |
|
wun0.1 |
|- ( ph -> U e. WUni ) |
2 |
|
wunfi.2 |
|- ( ph -> A C_ U ) |
3 |
|
wunfi.3 |
|- ( ph -> A e. Fin ) |
4 |
|
sseq1 |
|- ( x = (/) -> ( x C_ U <-> (/) C_ U ) ) |
5 |
|
eleq1 |
|- ( x = (/) -> ( x e. U <-> (/) e. U ) ) |
6 |
4 5
|
imbi12d |
|- ( x = (/) -> ( ( x C_ U -> x e. U ) <-> ( (/) C_ U -> (/) e. U ) ) ) |
7 |
6
|
imbi2d |
|- ( x = (/) -> ( ( ph -> ( x C_ U -> x e. U ) ) <-> ( ph -> ( (/) C_ U -> (/) e. U ) ) ) ) |
8 |
|
sseq1 |
|- ( x = y -> ( x C_ U <-> y C_ U ) ) |
9 |
|
eleq1 |
|- ( x = y -> ( x e. U <-> y e. U ) ) |
10 |
8 9
|
imbi12d |
|- ( x = y -> ( ( x C_ U -> x e. U ) <-> ( y C_ U -> y e. U ) ) ) |
11 |
10
|
imbi2d |
|- ( x = y -> ( ( ph -> ( x C_ U -> x e. U ) ) <-> ( ph -> ( y C_ U -> y e. U ) ) ) ) |
12 |
|
sseq1 |
|- ( x = ( y u. { z } ) -> ( x C_ U <-> ( y u. { z } ) C_ U ) ) |
13 |
|
eleq1 |
|- ( x = ( y u. { z } ) -> ( x e. U <-> ( y u. { z } ) e. U ) ) |
14 |
12 13
|
imbi12d |
|- ( x = ( y u. { z } ) -> ( ( x C_ U -> x e. U ) <-> ( ( y u. { z } ) C_ U -> ( y u. { z } ) e. U ) ) ) |
15 |
14
|
imbi2d |
|- ( x = ( y u. { z } ) -> ( ( ph -> ( x C_ U -> x e. U ) ) <-> ( ph -> ( ( y u. { z } ) C_ U -> ( y u. { z } ) e. U ) ) ) ) |
16 |
|
sseq1 |
|- ( x = A -> ( x C_ U <-> A C_ U ) ) |
17 |
|
eleq1 |
|- ( x = A -> ( x e. U <-> A e. U ) ) |
18 |
16 17
|
imbi12d |
|- ( x = A -> ( ( x C_ U -> x e. U ) <-> ( A C_ U -> A e. U ) ) ) |
19 |
18
|
imbi2d |
|- ( x = A -> ( ( ph -> ( x C_ U -> x e. U ) ) <-> ( ph -> ( A C_ U -> A e. U ) ) ) ) |
20 |
1
|
wun0 |
|- ( ph -> (/) e. U ) |
21 |
20
|
a1d |
|- ( ph -> ( (/) C_ U -> (/) e. U ) ) |
22 |
|
ssun1 |
|- y C_ ( y u. { z } ) |
23 |
|
sstr |
|- ( ( y C_ ( y u. { z } ) /\ ( y u. { z } ) C_ U ) -> y C_ U ) |
24 |
22 23
|
mpan |
|- ( ( y u. { z } ) C_ U -> y C_ U ) |
25 |
24
|
imim1i |
|- ( ( y C_ U -> y e. U ) -> ( ( y u. { z } ) C_ U -> y e. U ) ) |
26 |
1
|
adantr |
|- ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> U e. WUni ) |
27 |
|
simprr |
|- ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> y e. U ) |
28 |
|
simprl |
|- ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> ( y u. { z } ) C_ U ) |
29 |
28
|
unssbd |
|- ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> { z } C_ U ) |
30 |
|
vex |
|- z e. _V |
31 |
30
|
snss |
|- ( z e. U <-> { z } C_ U ) |
32 |
29 31
|
sylibr |
|- ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> z e. U ) |
33 |
26 32
|
wunsn |
|- ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> { z } e. U ) |
34 |
26 27 33
|
wunun |
|- ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> ( y u. { z } ) e. U ) |
35 |
34
|
exp32 |
|- ( ph -> ( ( y u. { z } ) C_ U -> ( y e. U -> ( y u. { z } ) e. U ) ) ) |
36 |
35
|
a2d |
|- ( ph -> ( ( ( y u. { z } ) C_ U -> y e. U ) -> ( ( y u. { z } ) C_ U -> ( y u. { z } ) e. U ) ) ) |
37 |
25 36
|
syl5 |
|- ( ph -> ( ( y C_ U -> y e. U ) -> ( ( y u. { z } ) C_ U -> ( y u. { z } ) e. U ) ) ) |
38 |
37
|
a2i |
|- ( ( ph -> ( y C_ U -> y e. U ) ) -> ( ph -> ( ( y u. { z } ) C_ U -> ( y u. { z } ) e. U ) ) ) |
39 |
38
|
a1i |
|- ( y e. Fin -> ( ( ph -> ( y C_ U -> y e. U ) ) -> ( ph -> ( ( y u. { z } ) C_ U -> ( y u. { z } ) e. U ) ) ) ) |
40 |
7 11 15 19 21 39
|
findcard2 |
|- ( A e. Fin -> ( ph -> ( A C_ U -> A e. U ) ) ) |
41 |
3 40
|
mpcom |
|- ( ph -> ( A C_ U -> A e. U ) ) |
42 |
2 41
|
mpd |
|- ( ph -> A e. U ) |