Step |
Hyp |
Ref |
Expression |
1 |
|
cnveq |
|- ( x = v -> `' x = `' v ) |
2 |
1
|
eqeq2d |
|- ( x = v -> ( z = `' x <-> z = `' v ) ) |
3 |
2
|
cbvrexvw |
|- ( E. x e. A z = `' x <-> E. v e. A z = `' v ) |
4 |
|
cnveq |
|- ( f = v -> `' f = `' v ) |
5 |
4
|
funeqd |
|- ( f = v -> ( Fun `' f <-> Fun `' v ) ) |
6 |
|
sseq1 |
|- ( f = v -> ( f C_ g <-> v C_ g ) ) |
7 |
|
sseq2 |
|- ( f = v -> ( g C_ f <-> g C_ v ) ) |
8 |
6 7
|
orbi12d |
|- ( f = v -> ( ( f C_ g \/ g C_ f ) <-> ( v C_ g \/ g C_ v ) ) ) |
9 |
8
|
ralbidv |
|- ( f = v -> ( A. g e. A ( f C_ g \/ g C_ f ) <-> A. g e. A ( v C_ g \/ g C_ v ) ) ) |
10 |
5 9
|
anbi12d |
|- ( f = v -> ( ( Fun `' f /\ A. g e. A ( f C_ g \/ g C_ f ) ) <-> ( Fun `' v /\ A. g e. A ( v C_ g \/ g C_ v ) ) ) ) |
11 |
10
|
rspcv |
|- ( v e. A -> ( A. f e. A ( Fun `' f /\ A. g e. A ( f C_ g \/ g C_ f ) ) -> ( Fun `' v /\ A. g e. A ( v C_ g \/ g C_ v ) ) ) ) |
12 |
|
funeq |
|- ( z = `' v -> ( Fun z <-> Fun `' v ) ) |
13 |
12
|
biimprcd |
|- ( Fun `' v -> ( z = `' v -> Fun z ) ) |
14 |
|
sseq2 |
|- ( g = x -> ( v C_ g <-> v C_ x ) ) |
15 |
|
sseq1 |
|- ( g = x -> ( g C_ v <-> x C_ v ) ) |
16 |
14 15
|
orbi12d |
|- ( g = x -> ( ( v C_ g \/ g C_ v ) <-> ( v C_ x \/ x C_ v ) ) ) |
17 |
16
|
rspcv |
|- ( x e. A -> ( A. g e. A ( v C_ g \/ g C_ v ) -> ( v C_ x \/ x C_ v ) ) ) |
18 |
|
cnvss |
|- ( v C_ x -> `' v C_ `' x ) |
19 |
|
cnvss |
|- ( x C_ v -> `' x C_ `' v ) |
20 |
18 19
|
orim12i |
|- ( ( v C_ x \/ x C_ v ) -> ( `' v C_ `' x \/ `' x C_ `' v ) ) |
21 |
|
sseq12 |
|- ( ( z = `' v /\ w = `' x ) -> ( z C_ w <-> `' v C_ `' x ) ) |
22 |
21
|
ancoms |
|- ( ( w = `' x /\ z = `' v ) -> ( z C_ w <-> `' v C_ `' x ) ) |
23 |
|
sseq12 |
|- ( ( w = `' x /\ z = `' v ) -> ( w C_ z <-> `' x C_ `' v ) ) |
24 |
22 23
|
orbi12d |
|- ( ( w = `' x /\ z = `' v ) -> ( ( z C_ w \/ w C_ z ) <-> ( `' v C_ `' x \/ `' x C_ `' v ) ) ) |
25 |
20 24
|
syl5ibrcom |
|- ( ( v C_ x \/ x C_ v ) -> ( ( w = `' x /\ z = `' v ) -> ( z C_ w \/ w C_ z ) ) ) |
26 |
25
|
expd |
|- ( ( v C_ x \/ x C_ v ) -> ( w = `' x -> ( z = `' v -> ( z C_ w \/ w C_ z ) ) ) ) |
27 |
17 26
|
syl6com |
|- ( A. g e. A ( v C_ g \/ g C_ v ) -> ( x e. A -> ( w = `' x -> ( z = `' v -> ( z C_ w \/ w C_ z ) ) ) ) ) |
28 |
27
|
rexlimdv |
|- ( A. g e. A ( v C_ g \/ g C_ v ) -> ( E. x e. A w = `' x -> ( z = `' v -> ( z C_ w \/ w C_ z ) ) ) ) |
29 |
28
|
com23 |
|- ( A. g e. A ( v C_ g \/ g C_ v ) -> ( z = `' v -> ( E. x e. A w = `' x -> ( z C_ w \/ w C_ z ) ) ) ) |
30 |
29
|
alrimdv |
|- ( A. g e. A ( v C_ g \/ g C_ v ) -> ( z = `' v -> A. w ( E. x e. A w = `' x -> ( z C_ w \/ w C_ z ) ) ) ) |
31 |
13 30
|
anim12ii |
|- ( ( Fun `' v /\ A. g e. A ( v C_ g \/ g C_ v ) ) -> ( z = `' v -> ( Fun z /\ A. w ( E. x e. A w = `' x -> ( z C_ w \/ w C_ z ) ) ) ) ) |
32 |
11 31
|
syl6com |
|- ( A. f e. A ( Fun `' f /\ A. g e. A ( f C_ g \/ g C_ f ) ) -> ( v e. A -> ( z = `' v -> ( Fun z /\ A. w ( E. x e. A w = `' x -> ( z C_ w \/ w C_ z ) ) ) ) ) ) |
33 |
32
|
rexlimdv |
|- ( A. f e. A ( Fun `' f /\ A. g e. A ( f C_ g \/ g C_ f ) ) -> ( E. v e. A z = `' v -> ( Fun z /\ A. w ( E. x e. A w = `' x -> ( z C_ w \/ w C_ z ) ) ) ) ) |
34 |
3 33
|
syl5bi |
|- ( A. f e. A ( Fun `' f /\ A. g e. A ( f C_ g \/ g C_ f ) ) -> ( E. x e. A z = `' x -> ( Fun z /\ A. w ( E. x e. A w = `' x -> ( z C_ w \/ w C_ z ) ) ) ) ) |
35 |
34
|
alrimiv |
|- ( A. f e. A ( Fun `' f /\ A. g e. A ( f C_ g \/ g C_ f ) ) -> A. z ( E. x e. A z = `' x -> ( Fun z /\ A. w ( E. x e. A w = `' x -> ( z C_ w \/ w C_ z ) ) ) ) ) |
36 |
|
df-ral |
|- ( A. z e. { y | E. x e. A y = `' x } ( Fun z /\ A. w e. { y | E. x e. A y = `' x } ( z C_ w \/ w C_ z ) ) <-> A. z ( z e. { y | E. x e. A y = `' x } -> ( Fun z /\ A. w e. { y | E. x e. A y = `' x } ( z C_ w \/ w C_ z ) ) ) ) |
37 |
|
vex |
|- z e. _V |
38 |
|
eqeq1 |
|- ( y = z -> ( y = `' x <-> z = `' x ) ) |
39 |
38
|
rexbidv |
|- ( y = z -> ( E. x e. A y = `' x <-> E. x e. A z = `' x ) ) |
40 |
37 39
|
elab |
|- ( z e. { y | E. x e. A y = `' x } <-> E. x e. A z = `' x ) |
41 |
|
eqeq1 |
|- ( y = w -> ( y = `' x <-> w = `' x ) ) |
42 |
41
|
rexbidv |
|- ( y = w -> ( E. x e. A y = `' x <-> E. x e. A w = `' x ) ) |
43 |
42
|
ralab |
|- ( A. w e. { y | E. x e. A y = `' x } ( z C_ w \/ w C_ z ) <-> A. w ( E. x e. A w = `' x -> ( z C_ w \/ w C_ z ) ) ) |
44 |
43
|
anbi2i |
|- ( ( Fun z /\ A. w e. { y | E. x e. A y = `' x } ( z C_ w \/ w C_ z ) ) <-> ( Fun z /\ A. w ( E. x e. A w = `' x -> ( z C_ w \/ w C_ z ) ) ) ) |
45 |
40 44
|
imbi12i |
|- ( ( z e. { y | E. x e. A y = `' x } -> ( Fun z /\ A. w e. { y | E. x e. A y = `' x } ( z C_ w \/ w C_ z ) ) ) <-> ( E. x e. A z = `' x -> ( Fun z /\ A. w ( E. x e. A w = `' x -> ( z C_ w \/ w C_ z ) ) ) ) ) |
46 |
45
|
albii |
|- ( A. z ( z e. { y | E. x e. A y = `' x } -> ( Fun z /\ A. w e. { y | E. x e. A y = `' x } ( z C_ w \/ w C_ z ) ) ) <-> A. z ( E. x e. A z = `' x -> ( Fun z /\ A. w ( E. x e. A w = `' x -> ( z C_ w \/ w C_ z ) ) ) ) ) |
47 |
36 46
|
bitr2i |
|- ( A. z ( E. x e. A z = `' x -> ( Fun z /\ A. w ( E. x e. A w = `' x -> ( z C_ w \/ w C_ z ) ) ) ) <-> A. z e. { y | E. x e. A y = `' x } ( Fun z /\ A. w e. { y | E. x e. A y = `' x } ( z C_ w \/ w C_ z ) ) ) |
48 |
35 47
|
sylib |
|- ( A. f e. A ( Fun `' f /\ A. g e. A ( f C_ g \/ g C_ f ) ) -> A. z e. { y | E. x e. A y = `' x } ( Fun z /\ A. w e. { y | E. x e. A y = `' x } ( z C_ w \/ w C_ z ) ) ) |
49 |
|
fununi |
|- ( A. z e. { y | E. x e. A y = `' x } ( Fun z /\ A. w e. { y | E. x e. A y = `' x } ( z C_ w \/ w C_ z ) ) -> Fun U. { y | E. x e. A y = `' x } ) |
50 |
48 49
|
syl |
|- ( A. f e. A ( Fun `' f /\ A. g e. A ( f C_ g \/ g C_ f ) ) -> Fun U. { y | E. x e. A y = `' x } ) |
51 |
|
cnvuni |
|- `' U. A = U_ x e. A `' x |
52 |
|
vex |
|- x e. _V |
53 |
52
|
cnvex |
|- `' x e. _V |
54 |
53
|
dfiun2 |
|- U_ x e. A `' x = U. { y | E. x e. A y = `' x } |
55 |
51 54
|
eqtri |
|- `' U. A = U. { y | E. x e. A y = `' x } |
56 |
55
|
funeqi |
|- ( Fun `' U. A <-> Fun U. { y | E. x e. A y = `' x } ) |
57 |
50 56
|
sylibr |
|- ( A. f e. A ( Fun `' f /\ A. g e. A ( f C_ g \/ g C_ f ) ) -> Fun `' U. A ) |