Step |
Hyp |
Ref |
Expression |
1 |
|
caofref.1 |
|- ( ph -> A e. V ) |
2 |
|
caofref.2 |
|- ( ph -> F : A --> S ) |
3 |
|
caofcom.3 |
|- ( ph -> G : A --> S ) |
4 |
|
caofass.4 |
|- ( ph -> H : A --> S ) |
5 |
|
caoftrn.5 |
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x R y /\ y T z ) -> x U z ) ) |
6 |
5
|
ralrimivvva |
|- ( ph -> A. x e. S A. y e. S A. z e. S ( ( x R y /\ y T z ) -> x U z ) ) |
7 |
6
|
adantr |
|- ( ( ph /\ w e. A ) -> A. x e. S A. y e. S A. z e. S ( ( x R y /\ y T z ) -> x U z ) ) |
8 |
2
|
ffvelrnda |
|- ( ( ph /\ w e. A ) -> ( F ` w ) e. S ) |
9 |
3
|
ffvelrnda |
|- ( ( ph /\ w e. A ) -> ( G ` w ) e. S ) |
10 |
4
|
ffvelrnda |
|- ( ( ph /\ w e. A ) -> ( H ` w ) e. S ) |
11 |
|
breq1 |
|- ( x = ( F ` w ) -> ( x R y <-> ( F ` w ) R y ) ) |
12 |
11
|
anbi1d |
|- ( x = ( F ` w ) -> ( ( x R y /\ y T z ) <-> ( ( F ` w ) R y /\ y T z ) ) ) |
13 |
|
breq1 |
|- ( x = ( F ` w ) -> ( x U z <-> ( F ` w ) U z ) ) |
14 |
12 13
|
imbi12d |
|- ( x = ( F ` w ) -> ( ( ( x R y /\ y T z ) -> x U z ) <-> ( ( ( F ` w ) R y /\ y T z ) -> ( F ` w ) U z ) ) ) |
15 |
|
breq2 |
|- ( y = ( G ` w ) -> ( ( F ` w ) R y <-> ( F ` w ) R ( G ` w ) ) ) |
16 |
|
breq1 |
|- ( y = ( G ` w ) -> ( y T z <-> ( G ` w ) T z ) ) |
17 |
15 16
|
anbi12d |
|- ( y = ( G ` w ) -> ( ( ( F ` w ) R y /\ y T z ) <-> ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T z ) ) ) |
18 |
17
|
imbi1d |
|- ( y = ( G ` w ) -> ( ( ( ( F ` w ) R y /\ y T z ) -> ( F ` w ) U z ) <-> ( ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T z ) -> ( F ` w ) U z ) ) ) |
19 |
|
breq2 |
|- ( z = ( H ` w ) -> ( ( G ` w ) T z <-> ( G ` w ) T ( H ` w ) ) ) |
20 |
19
|
anbi2d |
|- ( z = ( H ` w ) -> ( ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T z ) <-> ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T ( H ` w ) ) ) ) |
21 |
|
breq2 |
|- ( z = ( H ` w ) -> ( ( F ` w ) U z <-> ( F ` w ) U ( H ` w ) ) ) |
22 |
20 21
|
imbi12d |
|- ( z = ( H ` w ) -> ( ( ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T z ) -> ( F ` w ) U z ) <-> ( ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T ( H ` w ) ) -> ( F ` w ) U ( H ` w ) ) ) ) |
23 |
14 18 22
|
rspc3v |
|- ( ( ( F ` w ) e. S /\ ( G ` w ) e. S /\ ( H ` w ) e. S ) -> ( A. x e. S A. y e. S A. z e. S ( ( x R y /\ y T z ) -> x U z ) -> ( ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T ( H ` w ) ) -> ( F ` w ) U ( H ` w ) ) ) ) |
24 |
8 9 10 23
|
syl3anc |
|- ( ( ph /\ w e. A ) -> ( A. x e. S A. y e. S A. z e. S ( ( x R y /\ y T z ) -> x U z ) -> ( ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T ( H ` w ) ) -> ( F ` w ) U ( H ` w ) ) ) ) |
25 |
7 24
|
mpd |
|- ( ( ph /\ w e. A ) -> ( ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T ( H ` w ) ) -> ( F ` w ) U ( H ` w ) ) ) |
26 |
25
|
ralimdva |
|- ( ph -> ( A. w e. A ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T ( H ` w ) ) -> A. w e. A ( F ` w ) U ( H ` w ) ) ) |
27 |
2
|
ffnd |
|- ( ph -> F Fn A ) |
28 |
3
|
ffnd |
|- ( ph -> G Fn A ) |
29 |
|
inidm |
|- ( A i^i A ) = A |
30 |
|
eqidd |
|- ( ( ph /\ w e. A ) -> ( F ` w ) = ( F ` w ) ) |
31 |
|
eqidd |
|- ( ( ph /\ w e. A ) -> ( G ` w ) = ( G ` w ) ) |
32 |
27 28 1 1 29 30 31
|
ofrfval |
|- ( ph -> ( F oR R G <-> A. w e. A ( F ` w ) R ( G ` w ) ) ) |
33 |
4
|
ffnd |
|- ( ph -> H Fn A ) |
34 |
|
eqidd |
|- ( ( ph /\ w e. A ) -> ( H ` w ) = ( H ` w ) ) |
35 |
28 33 1 1 29 31 34
|
ofrfval |
|- ( ph -> ( G oR T H <-> A. w e. A ( G ` w ) T ( H ` w ) ) ) |
36 |
32 35
|
anbi12d |
|- ( ph -> ( ( F oR R G /\ G oR T H ) <-> ( A. w e. A ( F ` w ) R ( G ` w ) /\ A. w e. A ( G ` w ) T ( H ` w ) ) ) ) |
37 |
|
r19.26 |
|- ( A. w e. A ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T ( H ` w ) ) <-> ( A. w e. A ( F ` w ) R ( G ` w ) /\ A. w e. A ( G ` w ) T ( H ` w ) ) ) |
38 |
36 37
|
bitr4di |
|- ( ph -> ( ( F oR R G /\ G oR T H ) <-> A. w e. A ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T ( H ` w ) ) ) ) |
39 |
27 33 1 1 29 30 34
|
ofrfval |
|- ( ph -> ( F oR U H <-> A. w e. A ( F ` w ) U ( H ` w ) ) ) |
40 |
26 38 39
|
3imtr4d |
|- ( ph -> ( ( F oR R G /\ G oR T H ) -> F oR U H ) ) |