Step |
Hyp |
Ref |
Expression |
1 |
|
bren |
|- ( A ~~ B <-> E. f f : A -1-1-onto-> B ) |
2 |
|
bren |
|- ( C ~~ D <-> E. g g : C -1-1-onto-> D ) |
3 |
|
exdistrv |
|- ( E. f E. g ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) <-> ( E. f f : A -1-1-onto-> B /\ E. g g : C -1-1-onto-> D ) ) |
4 |
|
ovexd |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( A ^m C ) e. _V ) |
5 |
|
ovexd |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( B ^m D ) e. _V ) |
6 |
|
elmapi |
|- ( x e. ( A ^m C ) -> x : C --> A ) |
7 |
|
f1of |
|- ( f : A -1-1-onto-> B -> f : A --> B ) |
8 |
7
|
adantr |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> f : A --> B ) |
9 |
|
fco |
|- ( ( f : A --> B /\ x : C --> A ) -> ( f o. x ) : C --> B ) |
10 |
8 9
|
sylan |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ x : C --> A ) -> ( f o. x ) : C --> B ) |
11 |
|
f1ocnv |
|- ( g : C -1-1-onto-> D -> `' g : D -1-1-onto-> C ) |
12 |
11
|
adantl |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> `' g : D -1-1-onto-> C ) |
13 |
|
f1of |
|- ( `' g : D -1-1-onto-> C -> `' g : D --> C ) |
14 |
12 13
|
syl |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> `' g : D --> C ) |
15 |
14
|
adantr |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ x : C --> A ) -> `' g : D --> C ) |
16 |
10 15
|
fcod |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ x : C --> A ) -> ( ( f o. x ) o. `' g ) : D --> B ) |
17 |
16
|
ex |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( x : C --> A -> ( ( f o. x ) o. `' g ) : D --> B ) ) |
18 |
6 17
|
syl5 |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( x e. ( A ^m C ) -> ( ( f o. x ) o. `' g ) : D --> B ) ) |
19 |
|
f1ofo |
|- ( f : A -1-1-onto-> B -> f : A -onto-> B ) |
20 |
19
|
adantr |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> f : A -onto-> B ) |
21 |
|
forn |
|- ( f : A -onto-> B -> ran f = B ) |
22 |
20 21
|
syl |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ran f = B ) |
23 |
|
vex |
|- f e. _V |
24 |
23
|
rnex |
|- ran f e. _V |
25 |
22 24
|
eqeltrrdi |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> B e. _V ) |
26 |
|
f1ofo |
|- ( g : C -1-1-onto-> D -> g : C -onto-> D ) |
27 |
26
|
adantl |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> g : C -onto-> D ) |
28 |
|
forn |
|- ( g : C -onto-> D -> ran g = D ) |
29 |
27 28
|
syl |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ran g = D ) |
30 |
|
vex |
|- g e. _V |
31 |
30
|
rnex |
|- ran g e. _V |
32 |
29 31
|
eqeltrrdi |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> D e. _V ) |
33 |
25 32
|
elmapd |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( ( ( f o. x ) o. `' g ) e. ( B ^m D ) <-> ( ( f o. x ) o. `' g ) : D --> B ) ) |
34 |
18 33
|
sylibrd |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( x e. ( A ^m C ) -> ( ( f o. x ) o. `' g ) e. ( B ^m D ) ) ) |
35 |
|
elmapi |
|- ( y e. ( B ^m D ) -> y : D --> B ) |
36 |
|
f1ocnv |
|- ( f : A -1-1-onto-> B -> `' f : B -1-1-onto-> A ) |
37 |
36
|
adantr |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> `' f : B -1-1-onto-> A ) |
38 |
|
f1of |
|- ( `' f : B -1-1-onto-> A -> `' f : B --> A ) |
39 |
37 38
|
syl |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> `' f : B --> A ) |
40 |
39
|
adantr |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ y : D --> B ) -> `' f : B --> A ) |
41 |
|
id |
|- ( y : D --> B -> y : D --> B ) |
42 |
|
f1of |
|- ( g : C -1-1-onto-> D -> g : C --> D ) |
43 |
42
|
adantl |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> g : C --> D ) |
44 |
|
fco |
|- ( ( y : D --> B /\ g : C --> D ) -> ( y o. g ) : C --> B ) |
45 |
41 43 44
|
syl2anr |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ y : D --> B ) -> ( y o. g ) : C --> B ) |
46 |
40 45
|
fcod |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ y : D --> B ) -> ( `' f o. ( y o. g ) ) : C --> A ) |
47 |
46
|
ex |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( y : D --> B -> ( `' f o. ( y o. g ) ) : C --> A ) ) |
48 |
35 47
|
syl5 |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( y e. ( B ^m D ) -> ( `' f o. ( y o. g ) ) : C --> A ) ) |
49 |
|
f1odm |
|- ( f : A -1-1-onto-> B -> dom f = A ) |
50 |
49
|
adantr |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> dom f = A ) |
51 |
23
|
dmex |
|- dom f e. _V |
52 |
50 51
|
eqeltrrdi |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> A e. _V ) |
53 |
|
f1odm |
|- ( g : C -1-1-onto-> D -> dom g = C ) |
54 |
53
|
adantl |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> dom g = C ) |
55 |
30
|
dmex |
|- dom g e. _V |
56 |
54 55
|
eqeltrrdi |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> C e. _V ) |
57 |
52 56
|
elmapd |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( ( `' f o. ( y o. g ) ) e. ( A ^m C ) <-> ( `' f o. ( y o. g ) ) : C --> A ) ) |
58 |
48 57
|
sylibrd |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( y e. ( B ^m D ) -> ( `' f o. ( y o. g ) ) e. ( A ^m C ) ) ) |
59 |
|
coass |
|- ( ( f o. `' f ) o. ( y o. g ) ) = ( f o. ( `' f o. ( y o. g ) ) ) |
60 |
|
f1ococnv2 |
|- ( f : A -1-1-onto-> B -> ( f o. `' f ) = ( _I |` B ) ) |
61 |
60
|
ad2antrr |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( f o. `' f ) = ( _I |` B ) ) |
62 |
61
|
coeq1d |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. `' f ) o. ( y o. g ) ) = ( ( _I |` B ) o. ( y o. g ) ) ) |
63 |
45
|
adantrl |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( y o. g ) : C --> B ) |
64 |
|
fcoi2 |
|- ( ( y o. g ) : C --> B -> ( ( _I |` B ) o. ( y o. g ) ) = ( y o. g ) ) |
65 |
63 64
|
syl |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( _I |` B ) o. ( y o. g ) ) = ( y o. g ) ) |
66 |
62 65
|
eqtrd |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. `' f ) o. ( y o. g ) ) = ( y o. g ) ) |
67 |
59 66
|
syl5eqr |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( f o. ( `' f o. ( y o. g ) ) ) = ( y o. g ) ) |
68 |
67
|
eqeq2d |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) = ( f o. ( `' f o. ( y o. g ) ) ) <-> ( f o. x ) = ( y o. g ) ) ) |
69 |
|
coass |
|- ( ( ( f o. x ) o. `' g ) o. g ) = ( ( f o. x ) o. ( `' g o. g ) ) |
70 |
|
f1ococnv1 |
|- ( g : C -1-1-onto-> D -> ( `' g o. g ) = ( _I |` C ) ) |
71 |
70
|
ad2antlr |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( `' g o. g ) = ( _I |` C ) ) |
72 |
71
|
coeq2d |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) o. ( `' g o. g ) ) = ( ( f o. x ) o. ( _I |` C ) ) ) |
73 |
10
|
adantrr |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( f o. x ) : C --> B ) |
74 |
|
fcoi1 |
|- ( ( f o. x ) : C --> B -> ( ( f o. x ) o. ( _I |` C ) ) = ( f o. x ) ) |
75 |
73 74
|
syl |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) o. ( _I |` C ) ) = ( f o. x ) ) |
76 |
72 75
|
eqtrd |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) o. ( `' g o. g ) ) = ( f o. x ) ) |
77 |
69 76
|
syl5eq |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( ( f o. x ) o. `' g ) o. g ) = ( f o. x ) ) |
78 |
77
|
eqeq2d |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( y o. g ) = ( ( ( f o. x ) o. `' g ) o. g ) <-> ( y o. g ) = ( f o. x ) ) ) |
79 |
|
eqcom |
|- ( ( y o. g ) = ( f o. x ) <-> ( f o. x ) = ( y o. g ) ) |
80 |
78 79
|
bitrdi |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( y o. g ) = ( ( ( f o. x ) o. `' g ) o. g ) <-> ( f o. x ) = ( y o. g ) ) ) |
81 |
68 80
|
bitr4d |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) = ( f o. ( `' f o. ( y o. g ) ) ) <-> ( y o. g ) = ( ( ( f o. x ) o. `' g ) o. g ) ) ) |
82 |
|
f1of1 |
|- ( f : A -1-1-onto-> B -> f : A -1-1-> B ) |
83 |
82
|
ad2antrr |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> f : A -1-1-> B ) |
84 |
|
simprl |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> x : C --> A ) |
85 |
46
|
adantrl |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( `' f o. ( y o. g ) ) : C --> A ) |
86 |
|
cocan1 |
|- ( ( f : A -1-1-> B /\ x : C --> A /\ ( `' f o. ( y o. g ) ) : C --> A ) -> ( ( f o. x ) = ( f o. ( `' f o. ( y o. g ) ) ) <-> x = ( `' f o. ( y o. g ) ) ) ) |
87 |
83 84 85 86
|
syl3anc |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) = ( f o. ( `' f o. ( y o. g ) ) ) <-> x = ( `' f o. ( y o. g ) ) ) ) |
88 |
27
|
adantr |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> g : C -onto-> D ) |
89 |
|
ffn |
|- ( y : D --> B -> y Fn D ) |
90 |
89
|
ad2antll |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> y Fn D ) |
91 |
16
|
adantrr |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) o. `' g ) : D --> B ) |
92 |
91
|
ffnd |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) o. `' g ) Fn D ) |
93 |
|
cocan2 |
|- ( ( g : C -onto-> D /\ y Fn D /\ ( ( f o. x ) o. `' g ) Fn D ) -> ( ( y o. g ) = ( ( ( f o. x ) o. `' g ) o. g ) <-> y = ( ( f o. x ) o. `' g ) ) ) |
94 |
88 90 92 93
|
syl3anc |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( y o. g ) = ( ( ( f o. x ) o. `' g ) o. g ) <-> y = ( ( f o. x ) o. `' g ) ) ) |
95 |
81 87 94
|
3bitr3d |
|- ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( x = ( `' f o. ( y o. g ) ) <-> y = ( ( f o. x ) o. `' g ) ) ) |
96 |
95
|
ex |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( ( x : C --> A /\ y : D --> B ) -> ( x = ( `' f o. ( y o. g ) ) <-> y = ( ( f o. x ) o. `' g ) ) ) ) |
97 |
6 35 96
|
syl2ani |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( ( x e. ( A ^m C ) /\ y e. ( B ^m D ) ) -> ( x = ( `' f o. ( y o. g ) ) <-> y = ( ( f o. x ) o. `' g ) ) ) ) |
98 |
4 5 34 58 97
|
en3d |
|- ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( A ^m C ) ~~ ( B ^m D ) ) |
99 |
98
|
exlimivv |
|- ( E. f E. g ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( A ^m C ) ~~ ( B ^m D ) ) |
100 |
3 99
|
sylbir |
|- ( ( E. f f : A -1-1-onto-> B /\ E. g g : C -1-1-onto-> D ) -> ( A ^m C ) ~~ ( B ^m D ) ) |
101 |
1 2 100
|
syl2anb |
|- ( ( A ~~ B /\ C ~~ D ) -> ( A ^m C ) ~~ ( B ^m D ) ) |