Step |
Hyp |
Ref |
Expression |
1 |
|
cnmpt21.j |
|- ( ph -> J e. ( TopOn ` X ) ) |
2 |
|
cnmpt21.k |
|- ( ph -> K e. ( TopOn ` Y ) ) |
3 |
|
cnmpt21.a |
|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) ) |
4 |
|
cnmpt2t.b |
|- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) ) |
5 |
|
cnmpt22.l |
|- ( ph -> L e. ( TopOn ` Z ) ) |
6 |
|
cnmpt22.m |
|- ( ph -> M e. ( TopOn ` W ) ) |
7 |
|
cnmpt22.c |
|- ( ph -> ( z e. Z , w e. W |-> C ) e. ( ( L tX M ) Cn N ) ) |
8 |
|
cnmpt22.d |
|- ( ( z = A /\ w = B ) -> C = D ) |
9 |
|
df-ov |
|- ( A ( z e. Z , w e. W |-> C ) B ) = ( ( z e. Z , w e. W |-> C ) ` <. A , B >. ) |
10 |
|
txtopon |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) ) |
11 |
1 2 10
|
syl2anc |
|- ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) ) |
12 |
|
cnf2 |
|- ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ L e. ( TopOn ` Z ) /\ ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) ) -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z ) |
13 |
11 5 3 12
|
syl3anc |
|- ( ph -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z ) |
14 |
|
eqid |
|- ( x e. X , y e. Y |-> A ) = ( x e. X , y e. Y |-> A ) |
15 |
14
|
fmpo |
|- ( A. x e. X A. y e. Y A e. Z <-> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z ) |
16 |
13 15
|
sylibr |
|- ( ph -> A. x e. X A. y e. Y A e. Z ) |
17 |
|
rsp2 |
|- ( A. x e. X A. y e. Y A e. Z -> ( ( x e. X /\ y e. Y ) -> A e. Z ) ) |
18 |
16 17
|
syl |
|- ( ph -> ( ( x e. X /\ y e. Y ) -> A e. Z ) ) |
19 |
18
|
3impib |
|- ( ( ph /\ x e. X /\ y e. Y ) -> A e. Z ) |
20 |
|
cnf2 |
|- ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ M e. ( TopOn ` W ) /\ ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) ) -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> W ) |
21 |
11 6 4 20
|
syl3anc |
|- ( ph -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> W ) |
22 |
|
eqid |
|- ( x e. X , y e. Y |-> B ) = ( x e. X , y e. Y |-> B ) |
23 |
22
|
fmpo |
|- ( A. x e. X A. y e. Y B e. W <-> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> W ) |
24 |
21 23
|
sylibr |
|- ( ph -> A. x e. X A. y e. Y B e. W ) |
25 |
|
rsp2 |
|- ( A. x e. X A. y e. Y B e. W -> ( ( x e. X /\ y e. Y ) -> B e. W ) ) |
26 |
24 25
|
syl |
|- ( ph -> ( ( x e. X /\ y e. Y ) -> B e. W ) ) |
27 |
26
|
3impib |
|- ( ( ph /\ x e. X /\ y e. Y ) -> B e. W ) |
28 |
19 27
|
jca |
|- ( ( ph /\ x e. X /\ y e. Y ) -> ( A e. Z /\ B e. W ) ) |
29 |
|
txtopon |
|- ( ( L e. ( TopOn ` Z ) /\ M e. ( TopOn ` W ) ) -> ( L tX M ) e. ( TopOn ` ( Z X. W ) ) ) |
30 |
5 6 29
|
syl2anc |
|- ( ph -> ( L tX M ) e. ( TopOn ` ( Z X. W ) ) ) |
31 |
|
cntop2 |
|- ( ( z e. Z , w e. W |-> C ) e. ( ( L tX M ) Cn N ) -> N e. Top ) |
32 |
7 31
|
syl |
|- ( ph -> N e. Top ) |
33 |
|
toptopon2 |
|- ( N e. Top <-> N e. ( TopOn ` U. N ) ) |
34 |
32 33
|
sylib |
|- ( ph -> N e. ( TopOn ` U. N ) ) |
35 |
|
cnf2 |
|- ( ( ( L tX M ) e. ( TopOn ` ( Z X. W ) ) /\ N e. ( TopOn ` U. N ) /\ ( z e. Z , w e. W |-> C ) e. ( ( L tX M ) Cn N ) ) -> ( z e. Z , w e. W |-> C ) : ( Z X. W ) --> U. N ) |
36 |
30 34 7 35
|
syl3anc |
|- ( ph -> ( z e. Z , w e. W |-> C ) : ( Z X. W ) --> U. N ) |
37 |
|
eqid |
|- ( z e. Z , w e. W |-> C ) = ( z e. Z , w e. W |-> C ) |
38 |
37
|
fmpo |
|- ( A. z e. Z A. w e. W C e. U. N <-> ( z e. Z , w e. W |-> C ) : ( Z X. W ) --> U. N ) |
39 |
36 38
|
sylibr |
|- ( ph -> A. z e. Z A. w e. W C e. U. N ) |
40 |
|
r2al |
|- ( A. z e. Z A. w e. W C e. U. N <-> A. z A. w ( ( z e. Z /\ w e. W ) -> C e. U. N ) ) |
41 |
39 40
|
sylib |
|- ( ph -> A. z A. w ( ( z e. Z /\ w e. W ) -> C e. U. N ) ) |
42 |
41
|
3ad2ant1 |
|- ( ( ph /\ x e. X /\ y e. Y ) -> A. z A. w ( ( z e. Z /\ w e. W ) -> C e. U. N ) ) |
43 |
|
eleq1 |
|- ( z = A -> ( z e. Z <-> A e. Z ) ) |
44 |
|
eleq1 |
|- ( w = B -> ( w e. W <-> B e. W ) ) |
45 |
43 44
|
bi2anan9 |
|- ( ( z = A /\ w = B ) -> ( ( z e. Z /\ w e. W ) <-> ( A e. Z /\ B e. W ) ) ) |
46 |
8
|
eleq1d |
|- ( ( z = A /\ w = B ) -> ( C e. U. N <-> D e. U. N ) ) |
47 |
45 46
|
imbi12d |
|- ( ( z = A /\ w = B ) -> ( ( ( z e. Z /\ w e. W ) -> C e. U. N ) <-> ( ( A e. Z /\ B e. W ) -> D e. U. N ) ) ) |
48 |
47
|
spc2gv |
|- ( ( A e. Z /\ B e. W ) -> ( A. z A. w ( ( z e. Z /\ w e. W ) -> C e. U. N ) -> ( ( A e. Z /\ B e. W ) -> D e. U. N ) ) ) |
49 |
28 42 28 48
|
syl3c |
|- ( ( ph /\ x e. X /\ y e. Y ) -> D e. U. N ) |
50 |
8 37
|
ovmpoga |
|- ( ( A e. Z /\ B e. W /\ D e. U. N ) -> ( A ( z e. Z , w e. W |-> C ) B ) = D ) |
51 |
19 27 49 50
|
syl3anc |
|- ( ( ph /\ x e. X /\ y e. Y ) -> ( A ( z e. Z , w e. W |-> C ) B ) = D ) |
52 |
9 51
|
eqtr3id |
|- ( ( ph /\ x e. X /\ y e. Y ) -> ( ( z e. Z , w e. W |-> C ) ` <. A , B >. ) = D ) |
53 |
52
|
mpoeq3dva |
|- ( ph -> ( x e. X , y e. Y |-> ( ( z e. Z , w e. W |-> C ) ` <. A , B >. ) ) = ( x e. X , y e. Y |-> D ) ) |
54 |
1 2 3 4
|
cnmpt2t |
|- ( ph -> ( x e. X , y e. Y |-> <. A , B >. ) e. ( ( J tX K ) Cn ( L tX M ) ) ) |
55 |
1 2 54 7
|
cnmpt21f |
|- ( ph -> ( x e. X , y e. Y |-> ( ( z e. Z , w e. W |-> C ) ` <. A , B >. ) ) e. ( ( J tX K ) Cn N ) ) |
56 |
53 55
|
eqeltrrd |
|- ( ph -> ( x e. X , y e. Y |-> D ) e. ( ( J tX K ) Cn N ) ) |