Step |
Hyp |
Ref |
Expression |
1 |
|
ofpreima.1 |
|- ( ph -> F : A --> B ) |
2 |
|
ofpreima.2 |
|- ( ph -> G : A --> C ) |
3 |
|
ofpreima.3 |
|- ( ph -> A e. V ) |
4 |
|
ofpreima.4 |
|- ( ph -> R Fn ( B X. C ) ) |
5 |
1 2 3 4
|
ofpreima |
|- ( ph -> ( `' ( F oF R G ) " D ) = U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) |
6 |
|
inundif |
|- ( ( ( `' R " D ) i^i ( ran F X. ran G ) ) u. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) = ( `' R " D ) |
7 |
|
iuneq1 |
|- ( ( ( ( `' R " D ) i^i ( ran F X. ran G ) ) u. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) = ( `' R " D ) -> U_ p e. ( ( ( `' R " D ) i^i ( ran F X. ran G ) ) u. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) |
8 |
6 7
|
ax-mp |
|- U_ p e. ( ( ( `' R " D ) i^i ( ran F X. ran G ) ) u. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) |
9 |
|
iunxun |
|- U_ p e. ( ( ( `' R " D ) i^i ( ran F X. ran G ) ) u. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) |
10 |
8 9
|
eqtr3i |
|- U_ p e. ( `' R " D ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) |
11 |
5 10
|
eqtrdi |
|- ( ph -> ( `' ( F oF R G ) " D ) = ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) ) |
12 |
|
simpr |
|- ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) |
13 |
12
|
eldifbd |
|- ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> -. p e. ( ran F X. ran G ) ) |
14 |
|
cnvimass |
|- ( `' R " D ) C_ dom R |
15 |
4
|
fndmd |
|- ( ph -> dom R = ( B X. C ) ) |
16 |
14 15
|
sseqtrid |
|- ( ph -> ( `' R " D ) C_ ( B X. C ) ) |
17 |
16
|
ssdifssd |
|- ( ph -> ( ( `' R " D ) \ ( ran F X. ran G ) ) C_ ( B X. C ) ) |
18 |
17
|
sselda |
|- ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> p e. ( B X. C ) ) |
19 |
|
1st2nd2 |
|- ( p e. ( B X. C ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. ) |
20 |
|
elxp6 |
|- ( p e. ( ran F X. ran G ) <-> ( p = <. ( 1st ` p ) , ( 2nd ` p ) >. /\ ( ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) ) ) |
21 |
20
|
simplbi2 |
|- ( p = <. ( 1st ` p ) , ( 2nd ` p ) >. -> ( ( ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) -> p e. ( ran F X. ran G ) ) ) |
22 |
18 19 21
|
3syl |
|- ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> ( ( ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) -> p e. ( ran F X. ran G ) ) ) |
23 |
13 22
|
mtod |
|- ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> -. ( ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) ) |
24 |
|
ianor |
|- ( -. ( ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) <-> ( -. ( 1st ` p ) e. ran F \/ -. ( 2nd ` p ) e. ran G ) ) |
25 |
23 24
|
sylib |
|- ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> ( -. ( 1st ` p ) e. ran F \/ -. ( 2nd ` p ) e. ran G ) ) |
26 |
|
disjsn |
|- ( ( ran F i^i { ( 1st ` p ) } ) = (/) <-> -. ( 1st ` p ) e. ran F ) |
27 |
|
disjsn |
|- ( ( ran G i^i { ( 2nd ` p ) } ) = (/) <-> -. ( 2nd ` p ) e. ran G ) |
28 |
26 27
|
orbi12i |
|- ( ( ( ran F i^i { ( 1st ` p ) } ) = (/) \/ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) <-> ( -. ( 1st ` p ) e. ran F \/ -. ( 2nd ` p ) e. ran G ) ) |
29 |
25 28
|
sylibr |
|- ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> ( ( ran F i^i { ( 1st ` p ) } ) = (/) \/ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) ) |
30 |
1
|
ffnd |
|- ( ph -> F Fn A ) |
31 |
|
dffn3 |
|- ( F Fn A <-> F : A --> ran F ) |
32 |
30 31
|
sylib |
|- ( ph -> F : A --> ran F ) |
33 |
2
|
ffnd |
|- ( ph -> G Fn A ) |
34 |
|
dffn3 |
|- ( G Fn A <-> G : A --> ran G ) |
35 |
33 34
|
sylib |
|- ( ph -> G : A --> ran G ) |
36 |
35
|
adantr |
|- ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> G : A --> ran G ) |
37 |
|
fimacnvdisj |
|- ( ( F : A --> ran F /\ ( ran F i^i { ( 1st ` p ) } ) = (/) ) -> ( `' F " { ( 1st ` p ) } ) = (/) ) |
38 |
|
ineq1 |
|- ( ( `' F " { ( 1st ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = ( (/) i^i ( `' G " { ( 2nd ` p ) } ) ) ) |
39 |
|
0in |
|- ( (/) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) |
40 |
38 39
|
eqtrdi |
|- ( ( `' F " { ( 1st ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) |
41 |
37 40
|
syl |
|- ( ( F : A --> ran F /\ ( ran F i^i { ( 1st ` p ) } ) = (/) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) |
42 |
41
|
ex |
|- ( F : A --> ran F -> ( ( ran F i^i { ( 1st ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) ) |
43 |
|
fimacnvdisj |
|- ( ( G : A --> ran G /\ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) -> ( `' G " { ( 2nd ` p ) } ) = (/) ) |
44 |
|
ineq2 |
|- ( ( `' G " { ( 2nd ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = ( ( `' F " { ( 1st ` p ) } ) i^i (/) ) ) |
45 |
|
in0 |
|- ( ( `' F " { ( 1st ` p ) } ) i^i (/) ) = (/) |
46 |
44 45
|
eqtrdi |
|- ( ( `' G " { ( 2nd ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) |
47 |
43 46
|
syl |
|- ( ( G : A --> ran G /\ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) |
48 |
47
|
ex |
|- ( G : A --> ran G -> ( ( ran G i^i { ( 2nd ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) ) |
49 |
42 48
|
jaao |
|- ( ( F : A --> ran F /\ G : A --> ran G ) -> ( ( ( ran F i^i { ( 1st ` p ) } ) = (/) \/ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) ) |
50 |
32 36 49
|
syl2an2r |
|- ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> ( ( ( ran F i^i { ( 1st ` p ) } ) = (/) \/ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) ) |
51 |
29 50
|
mpd |
|- ( ( ph /\ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) |
52 |
51
|
iuneq2dv |
|- ( ph -> U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) (/) ) |
53 |
|
iun0 |
|- U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) (/) = (/) |
54 |
52 53
|
eqtrdi |
|- ( ph -> U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) |
55 |
54
|
uneq2d |
|- ( ph -> ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) = ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. (/) ) ) |
56 |
|
un0 |
|- ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. (/) ) = U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) |
57 |
55 56
|
eqtrdi |
|- ( ph -> ( U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) u. U_ p e. ( ( `' R " D ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) = U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) |
58 |
11 57
|
eqtrd |
|- ( ph -> ( `' ( F oF R G ) " D ) = U_ p e. ( ( `' R " D ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) |