Step |
Hyp |
Ref |
Expression |
1 |
|
cnfcom3c.s |
|- S = dom ( _om CNF A ) |
2 |
|
cnfcom3c.f |
|- F = ( `' ( _om CNF A ) ` b ) |
3 |
|
cnfcom3c.g |
|- G = OrdIso ( _E , ( F supp (/) ) ) |
4 |
|
cnfcom3c.h |
|- H = seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) ) |
5 |
|
cnfcom3c.t |
|- T = seqom ( ( k e. _V , f e. _V |-> K ) , (/) ) |
6 |
|
cnfcom3c.m |
|- M = ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) |
7 |
|
cnfcom3c.k |
|- K = ( ( x e. M |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( M +o x ) ) ) |
8 |
|
cnfcom3c.w |
|- W = ( G ` U. dom G ) |
9 |
|
cnfcom3c.x |
|- X = ( u e. ( F ` W ) , v e. ( _om ^o W ) |-> ( ( ( F ` W ) .o v ) +o u ) ) |
10 |
|
cnfcom3c.y |
|- Y = ( u e. ( F ` W ) , v e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o u ) +o v ) ) |
11 |
|
cnfcom3c.n |
|- N = ( ( X o. `' Y ) o. ( T ` dom G ) ) |
12 |
|
cnfcom3c.l |
|- L = ( b e. ( _om ^o A ) |-> N ) |
13 |
|
simp1 |
|- ( ( A e. On /\ b e. A /\ _om C_ b ) -> A e. On ) |
14 |
|
omelon |
|- _om e. On |
15 |
|
1onn |
|- 1o e. _om |
16 |
|
ondif2 |
|- ( _om e. ( On \ 2o ) <-> ( _om e. On /\ 1o e. _om ) ) |
17 |
14 15 16
|
mpbir2an |
|- _om e. ( On \ 2o ) |
18 |
|
oeworde |
|- ( ( _om e. ( On \ 2o ) /\ A e. On ) -> A C_ ( _om ^o A ) ) |
19 |
17 13 18
|
sylancr |
|- ( ( A e. On /\ b e. A /\ _om C_ b ) -> A C_ ( _om ^o A ) ) |
20 |
|
simp2 |
|- ( ( A e. On /\ b e. A /\ _om C_ b ) -> b e. A ) |
21 |
19 20
|
sseldd |
|- ( ( A e. On /\ b e. A /\ _om C_ b ) -> b e. ( _om ^o A ) ) |
22 |
|
simp3 |
|- ( ( A e. On /\ b e. A /\ _om C_ b ) -> _om C_ b ) |
23 |
1 13 21 2 3 4 5 6 7 8 22
|
cnfcom3lem |
|- ( ( A e. On /\ b e. A /\ _om C_ b ) -> W e. ( On \ 1o ) ) |
24 |
1 13 21 2 3 4 5 6 7 8 22 9 10 11
|
cnfcom3 |
|- ( ( A e. On /\ b e. A /\ _om C_ b ) -> N : b -1-1-onto-> ( _om ^o W ) ) |
25 |
|
f1of |
|- ( N : b -1-1-onto-> ( _om ^o W ) -> N : b --> ( _om ^o W ) ) |
26 |
24 25
|
syl |
|- ( ( A e. On /\ b e. A /\ _om C_ b ) -> N : b --> ( _om ^o W ) ) |
27 |
|
vex |
|- b e. _V |
28 |
|
fex |
|- ( ( N : b --> ( _om ^o W ) /\ b e. _V ) -> N e. _V ) |
29 |
26 27 28
|
sylancl |
|- ( ( A e. On /\ b e. A /\ _om C_ b ) -> N e. _V ) |
30 |
12
|
fvmpt2 |
|- ( ( b e. ( _om ^o A ) /\ N e. _V ) -> ( L ` b ) = N ) |
31 |
21 29 30
|
syl2anc |
|- ( ( A e. On /\ b e. A /\ _om C_ b ) -> ( L ` b ) = N ) |
32 |
|
f1oeq1 |
|- ( ( L ` b ) = N -> ( ( L ` b ) : b -1-1-onto-> ( _om ^o W ) <-> N : b -1-1-onto-> ( _om ^o W ) ) ) |
33 |
31 32
|
syl |
|- ( ( A e. On /\ b e. A /\ _om C_ b ) -> ( ( L ` b ) : b -1-1-onto-> ( _om ^o W ) <-> N : b -1-1-onto-> ( _om ^o W ) ) ) |
34 |
24 33
|
mpbird |
|- ( ( A e. On /\ b e. A /\ _om C_ b ) -> ( L ` b ) : b -1-1-onto-> ( _om ^o W ) ) |
35 |
|
oveq2 |
|- ( w = W -> ( _om ^o w ) = ( _om ^o W ) ) |
36 |
35
|
f1oeq3d |
|- ( w = W -> ( ( L ` b ) : b -1-1-onto-> ( _om ^o w ) <-> ( L ` b ) : b -1-1-onto-> ( _om ^o W ) ) ) |
37 |
36
|
rspcev |
|- ( ( W e. ( On \ 1o ) /\ ( L ` b ) : b -1-1-onto-> ( _om ^o W ) ) -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) |
38 |
23 34 37
|
syl2anc |
|- ( ( A e. On /\ b e. A /\ _om C_ b ) -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) |
39 |
38
|
3expia |
|- ( ( A e. On /\ b e. A ) -> ( _om C_ b -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) |
40 |
39
|
ralrimiva |
|- ( A e. On -> A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) |
41 |
|
ovex |
|- ( _om ^o A ) e. _V |
42 |
41
|
mptex |
|- ( b e. ( _om ^o A ) |-> N ) e. _V |
43 |
12 42
|
eqeltri |
|- L e. _V |
44 |
|
nfmpt1 |
|- F/_ b ( b e. ( _om ^o A ) |-> N ) |
45 |
12 44
|
nfcxfr |
|- F/_ b L |
46 |
45
|
nfeq2 |
|- F/ b g = L |
47 |
|
fveq1 |
|- ( g = L -> ( g ` b ) = ( L ` b ) ) |
48 |
|
f1oeq1 |
|- ( ( g ` b ) = ( L ` b ) -> ( ( g ` b ) : b -1-1-onto-> ( _om ^o w ) <-> ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) |
49 |
47 48
|
syl |
|- ( g = L -> ( ( g ` b ) : b -1-1-onto-> ( _om ^o w ) <-> ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) |
50 |
49
|
rexbidv |
|- ( g = L -> ( E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( _om ^o w ) <-> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) |
51 |
50
|
imbi2d |
|- ( g = L -> ( ( _om C_ b -> E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( _om ^o w ) ) <-> ( _om C_ b -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) ) |
52 |
46 51
|
ralbid |
|- ( g = L -> ( A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( _om ^o w ) ) <-> A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) ) |
53 |
43 52
|
spcev |
|- ( A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) -> E. g A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) |
54 |
40 53
|
syl |
|- ( A e. On -> E. g A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) |