Step |
Hyp |
Ref |
Expression |
1 |
|
ttukeylem.1 |
|- ( ph -> F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) ) |
2 |
|
ttukeylem.2 |
|- ( ph -> B e. A ) |
3 |
|
ttukeylem.3 |
|- ( ph -> A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) |
4 |
|
ttukeylem.4 |
|- G = recs ( ( z e. _V |-> if ( dom z = U. dom z , if ( dom z = (/) , B , U. ran z ) , ( ( z ` U. dom z ) u. if ( ( ( z ` U. dom z ) u. { ( F ` U. dom z ) } ) e. A , { ( F ` U. dom z ) } , (/) ) ) ) ) ) |
5 |
|
fvex |
|- ( card ` ( U. A \ B ) ) e. _V |
6 |
5
|
sucid |
|- ( card ` ( U. A \ B ) ) e. suc ( card ` ( U. A \ B ) ) |
7 |
1 2 3 4
|
ttukeylem6 |
|- ( ( ph /\ ( card ` ( U. A \ B ) ) e. suc ( card ` ( U. A \ B ) ) ) -> ( G ` ( card ` ( U. A \ B ) ) ) e. A ) |
8 |
6 7
|
mpan2 |
|- ( ph -> ( G ` ( card ` ( U. A \ B ) ) ) e. A ) |
9 |
1 2 3 4
|
ttukeylem4 |
|- ( ph -> ( G ` (/) ) = B ) |
10 |
|
0elon |
|- (/) e. On |
11 |
|
cardon |
|- ( card ` ( U. A \ B ) ) e. On |
12 |
|
0ss |
|- (/) C_ ( card ` ( U. A \ B ) ) |
13 |
10 11 12
|
3pm3.2i |
|- ( (/) e. On /\ ( card ` ( U. A \ B ) ) e. On /\ (/) C_ ( card ` ( U. A \ B ) ) ) |
14 |
1 2 3 4
|
ttukeylem5 |
|- ( ( ph /\ ( (/) e. On /\ ( card ` ( U. A \ B ) ) e. On /\ (/) C_ ( card ` ( U. A \ B ) ) ) ) -> ( G ` (/) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) ) |
15 |
13 14
|
mpan2 |
|- ( ph -> ( G ` (/) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) ) |
16 |
9 15
|
eqsstrrd |
|- ( ph -> B C_ ( G ` ( card ` ( U. A \ B ) ) ) ) |
17 |
|
simprr |
|- ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) |
18 |
|
ssun1 |
|- y C_ ( y u. B ) |
19 |
|
undif1 |
|- ( ( y \ B ) u. B ) = ( y u. B ) |
20 |
18 19
|
sseqtrri |
|- y C_ ( ( y \ B ) u. B ) |
21 |
|
simpl |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ph ) |
22 |
|
f1ocnv |
|- ( F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) -> `' F : ( U. A \ B ) -1-1-onto-> ( card ` ( U. A \ B ) ) ) |
23 |
|
f1of |
|- ( `' F : ( U. A \ B ) -1-1-onto-> ( card ` ( U. A \ B ) ) -> `' F : ( U. A \ B ) --> ( card ` ( U. A \ B ) ) ) |
24 |
1 22 23
|
3syl |
|- ( ph -> `' F : ( U. A \ B ) --> ( card ` ( U. A \ B ) ) ) |
25 |
24
|
adantr |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> `' F : ( U. A \ B ) --> ( card ` ( U. A \ B ) ) ) |
26 |
|
eldifi |
|- ( a e. ( y \ B ) -> a e. y ) |
27 |
26
|
ad2antll |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. y ) |
28 |
|
simprll |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> y e. A ) |
29 |
|
elunii |
|- ( ( a e. y /\ y e. A ) -> a e. U. A ) |
30 |
27 28 29
|
syl2anc |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. U. A ) |
31 |
|
eldifn |
|- ( a e. ( y \ B ) -> -. a e. B ) |
32 |
31
|
ad2antll |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> -. a e. B ) |
33 |
30 32
|
eldifd |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. ( U. A \ B ) ) |
34 |
25 33
|
ffvelrnd |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( `' F ` a ) e. ( card ` ( U. A \ B ) ) ) |
35 |
|
onelon |
|- ( ( ( card ` ( U. A \ B ) ) e. On /\ ( `' F ` a ) e. ( card ` ( U. A \ B ) ) ) -> ( `' F ` a ) e. On ) |
36 |
11 34 35
|
sylancr |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( `' F ` a ) e. On ) |
37 |
|
suceloni |
|- ( ( `' F ` a ) e. On -> suc ( `' F ` a ) e. On ) |
38 |
36 37
|
syl |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> suc ( `' F ` a ) e. On ) |
39 |
11
|
a1i |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( card ` ( U. A \ B ) ) e. On ) |
40 |
11
|
onordi |
|- Ord ( card ` ( U. A \ B ) ) |
41 |
|
ordsucss |
|- ( Ord ( card ` ( U. A \ B ) ) -> ( ( `' F ` a ) e. ( card ` ( U. A \ B ) ) -> suc ( `' F ` a ) C_ ( card ` ( U. A \ B ) ) ) ) |
42 |
40 34 41
|
mpsyl |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> suc ( `' F ` a ) C_ ( card ` ( U. A \ B ) ) ) |
43 |
1 2 3 4
|
ttukeylem5 |
|- ( ( ph /\ ( suc ( `' F ` a ) e. On /\ ( card ` ( U. A \ B ) ) e. On /\ suc ( `' F ` a ) C_ ( card ` ( U. A \ B ) ) ) ) -> ( G ` suc ( `' F ` a ) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) ) |
44 |
21 38 39 42 43
|
syl13anc |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` suc ( `' F ` a ) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) ) |
45 |
|
ssun2 |
|- if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) C_ ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) |
46 |
|
eloni |
|- ( ( `' F ` a ) e. On -> Ord ( `' F ` a ) ) |
47 |
|
ordunisuc |
|- ( Ord ( `' F ` a ) -> U. suc ( `' F ` a ) = ( `' F ` a ) ) |
48 |
36 46 47
|
3syl |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> U. suc ( `' F ` a ) = ( `' F ` a ) ) |
49 |
48
|
fveq2d |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( F ` U. suc ( `' F ` a ) ) = ( F ` ( `' F ` a ) ) ) |
50 |
1
|
adantr |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) ) |
51 |
|
f1ocnvfv2 |
|- ( ( F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) /\ a e. ( U. A \ B ) ) -> ( F ` ( `' F ` a ) ) = a ) |
52 |
50 33 51
|
syl2anc |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( F ` ( `' F ` a ) ) = a ) |
53 |
49 52
|
eqtr2d |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a = ( F ` U. suc ( `' F ` a ) ) ) |
54 |
|
velsn |
|- ( a e. { ( F ` U. suc ( `' F ` a ) ) } <-> a = ( F ` U. suc ( `' F ` a ) ) ) |
55 |
53 54
|
sylibr |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. { ( F ` U. suc ( `' F ` a ) ) } ) |
56 |
48
|
fveq2d |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` U. suc ( `' F ` a ) ) = ( G ` ( `' F ` a ) ) ) |
57 |
|
ordelss |
|- ( ( Ord ( card ` ( U. A \ B ) ) /\ ( `' F ` a ) e. ( card ` ( U. A \ B ) ) ) -> ( `' F ` a ) C_ ( card ` ( U. A \ B ) ) ) |
58 |
40 34 57
|
sylancr |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( `' F ` a ) C_ ( card ` ( U. A \ B ) ) ) |
59 |
1 2 3 4
|
ttukeylem5 |
|- ( ( ph /\ ( ( `' F ` a ) e. On /\ ( card ` ( U. A \ B ) ) e. On /\ ( `' F ` a ) C_ ( card ` ( U. A \ B ) ) ) ) -> ( G ` ( `' F ` a ) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) ) |
60 |
21 36 39 58 59
|
syl13anc |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` ( `' F ` a ) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) ) |
61 |
56 60
|
eqsstrd |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` U. suc ( `' F ` a ) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) ) |
62 |
|
simprlr |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) |
63 |
61 62
|
sstrd |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` U. suc ( `' F ` a ) ) C_ y ) |
64 |
53 27
|
eqeltrrd |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( F ` U. suc ( `' F ` a ) ) e. y ) |
65 |
64
|
snssd |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> { ( F ` U. suc ( `' F ` a ) ) } C_ y ) |
66 |
63 65
|
unssd |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) C_ y ) |
67 |
1 2 3
|
ttukeylem2 |
|- ( ( ph /\ ( y e. A /\ ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) C_ y ) ) -> ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A ) |
68 |
21 28 66 67
|
syl12anc |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A ) |
69 |
68
|
iftrued |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) = { ( F ` U. suc ( `' F ` a ) ) } ) |
70 |
55 69
|
eleqtrrd |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) |
71 |
45 70
|
sselid |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) ) |
72 |
1 2 3 4
|
ttukeylem3 |
|- ( ( ph /\ suc ( `' F ` a ) e. On ) -> ( G ` suc ( `' F ` a ) ) = if ( suc ( `' F ` a ) = U. suc ( `' F ` a ) , if ( suc ( `' F ` a ) = (/) , B , U. ( G " suc ( `' F ` a ) ) ) , ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) ) ) |
73 |
38 72
|
syldan |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` suc ( `' F ` a ) ) = if ( suc ( `' F ` a ) = U. suc ( `' F ` a ) , if ( suc ( `' F ` a ) = (/) , B , U. ( G " suc ( `' F ` a ) ) ) , ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) ) ) |
74 |
|
sucidg |
|- ( ( `' F ` a ) e. ( card ` ( U. A \ B ) ) -> ( `' F ` a ) e. suc ( `' F ` a ) ) |
75 |
34 74
|
syl |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( `' F ` a ) e. suc ( `' F ` a ) ) |
76 |
|
ordirr |
|- ( Ord ( `' F ` a ) -> -. ( `' F ` a ) e. ( `' F ` a ) ) |
77 |
36 46 76
|
3syl |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> -. ( `' F ` a ) e. ( `' F ` a ) ) |
78 |
|
nelne1 |
|- ( ( ( `' F ` a ) e. suc ( `' F ` a ) /\ -. ( `' F ` a ) e. ( `' F ` a ) ) -> suc ( `' F ` a ) =/= ( `' F ` a ) ) |
79 |
75 77 78
|
syl2anc |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> suc ( `' F ` a ) =/= ( `' F ` a ) ) |
80 |
79 48
|
neeqtrrd |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> suc ( `' F ` a ) =/= U. suc ( `' F ` a ) ) |
81 |
80
|
neneqd |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> -. suc ( `' F ` a ) = U. suc ( `' F ` a ) ) |
82 |
81
|
iffalsed |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> if ( suc ( `' F ` a ) = U. suc ( `' F ` a ) , if ( suc ( `' F ` a ) = (/) , B , U. ( G " suc ( `' F ` a ) ) ) , ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) ) = ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) ) |
83 |
73 82
|
eqtrd |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` suc ( `' F ` a ) ) = ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) ) |
84 |
71 83
|
eleqtrrd |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. ( G ` suc ( `' F ` a ) ) ) |
85 |
44 84
|
sseldd |
|- ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. ( G ` ( card ` ( U. A \ B ) ) ) ) |
86 |
85
|
expr |
|- ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> ( a e. ( y \ B ) -> a e. ( G ` ( card ` ( U. A \ B ) ) ) ) ) |
87 |
86
|
ssrdv |
|- ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> ( y \ B ) C_ ( G ` ( card ` ( U. A \ B ) ) ) ) |
88 |
16
|
adantr |
|- ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> B C_ ( G ` ( card ` ( U. A \ B ) ) ) ) |
89 |
87 88
|
unssd |
|- ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> ( ( y \ B ) u. B ) C_ ( G ` ( card ` ( U. A \ B ) ) ) ) |
90 |
20 89
|
sstrid |
|- ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> y C_ ( G ` ( card ` ( U. A \ B ) ) ) ) |
91 |
17 90
|
eqssd |
|- ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> ( G ` ( card ` ( U. A \ B ) ) ) = y ) |
92 |
91
|
expr |
|- ( ( ph /\ y e. A ) -> ( ( G ` ( card ` ( U. A \ B ) ) ) C_ y -> ( G ` ( card ` ( U. A \ B ) ) ) = y ) ) |
93 |
|
npss |
|- ( -. ( G ` ( card ` ( U. A \ B ) ) ) C. y <-> ( ( G ` ( card ` ( U. A \ B ) ) ) C_ y -> ( G ` ( card ` ( U. A \ B ) ) ) = y ) ) |
94 |
92 93
|
sylibr |
|- ( ( ph /\ y e. A ) -> -. ( G ` ( card ` ( U. A \ B ) ) ) C. y ) |
95 |
94
|
ralrimiva |
|- ( ph -> A. y e. A -. ( G ` ( card ` ( U. A \ B ) ) ) C. y ) |
96 |
|
sseq2 |
|- ( x = ( G ` ( card ` ( U. A \ B ) ) ) -> ( B C_ x <-> B C_ ( G ` ( card ` ( U. A \ B ) ) ) ) ) |
97 |
|
psseq1 |
|- ( x = ( G ` ( card ` ( U. A \ B ) ) ) -> ( x C. y <-> ( G ` ( card ` ( U. A \ B ) ) ) C. y ) ) |
98 |
97
|
notbid |
|- ( x = ( G ` ( card ` ( U. A \ B ) ) ) -> ( -. x C. y <-> -. ( G ` ( card ` ( U. A \ B ) ) ) C. y ) ) |
99 |
98
|
ralbidv |
|- ( x = ( G ` ( card ` ( U. A \ B ) ) ) -> ( A. y e. A -. x C. y <-> A. y e. A -. ( G ` ( card ` ( U. A \ B ) ) ) C. y ) ) |
100 |
96 99
|
anbi12d |
|- ( x = ( G ` ( card ` ( U. A \ B ) ) ) -> ( ( B C_ x /\ A. y e. A -. x C. y ) <-> ( B C_ ( G ` ( card ` ( U. A \ B ) ) ) /\ A. y e. A -. ( G ` ( card ` ( U. A \ B ) ) ) C. y ) ) ) |
101 |
100
|
rspcev |
|- ( ( ( G ` ( card ` ( U. A \ B ) ) ) e. A /\ ( B C_ ( G ` ( card ` ( U. A \ B ) ) ) /\ A. y e. A -. ( G ` ( card ` ( U. A \ B ) ) ) C. y ) ) -> E. x e. A ( B C_ x /\ A. y e. A -. x C. y ) ) |
102 |
8 16 95 101
|
syl12anc |
|- ( ph -> E. x e. A ( B C_ x /\ A. y e. A -. x C. y ) ) |