Step |
Hyp |
Ref |
Expression |
1 |
|
risset |
|- ( U. z e. A <-> E. x e. A x = U. z ) |
2 |
|
eqimss2 |
|- ( x = U. z -> U. z C_ x ) |
3 |
|
unissb |
|- ( U. z C_ x <-> A. u e. z u C_ x ) |
4 |
2 3
|
sylib |
|- ( x = U. z -> A. u e. z u C_ x ) |
5 |
|
vex |
|- x e. _V |
6 |
5
|
brrpss |
|- ( u [C.] x <-> u C. x ) |
7 |
6
|
orbi1i |
|- ( ( u [C.] x \/ u = x ) <-> ( u C. x \/ u = x ) ) |
8 |
|
sspss |
|- ( u C_ x <-> ( u C. x \/ u = x ) ) |
9 |
7 8
|
bitr4i |
|- ( ( u [C.] x \/ u = x ) <-> u C_ x ) |
10 |
9
|
ralbii |
|- ( A. u e. z ( u [C.] x \/ u = x ) <-> A. u e. z u C_ x ) |
11 |
4 10
|
sylibr |
|- ( x = U. z -> A. u e. z ( u [C.] x \/ u = x ) ) |
12 |
11
|
reximi |
|- ( E. x e. A x = U. z -> E. x e. A A. u e. z ( u [C.] x \/ u = x ) ) |
13 |
1 12
|
sylbi |
|- ( U. z e. A -> E. x e. A A. u e. z ( u [C.] x \/ u = x ) ) |
14 |
13
|
imim2i |
|- ( ( ( z C_ A /\ [C.] Or z ) -> U. z e. A ) -> ( ( z C_ A /\ [C.] Or z ) -> E. x e. A A. u e. z ( u [C.] x \/ u = x ) ) ) |
15 |
14
|
alimi |
|- ( A. z ( ( z C_ A /\ [C.] Or z ) -> U. z e. A ) -> A. z ( ( z C_ A /\ [C.] Or z ) -> E. x e. A A. u e. z ( u [C.] x \/ u = x ) ) ) |
16 |
|
porpss |
|- [C.] Po A |
17 |
|
zorn2g |
|- ( ( A e. dom card /\ [C.] Po A /\ A. z ( ( z C_ A /\ [C.] Or z ) -> E. x e. A A. u e. z ( u [C.] x \/ u = x ) ) ) -> E. x e. A A. y e. A -. x [C.] y ) |
18 |
16 17
|
mp3an2 |
|- ( ( A e. dom card /\ A. z ( ( z C_ A /\ [C.] Or z ) -> E. x e. A A. u e. z ( u [C.] x \/ u = x ) ) ) -> E. x e. A A. y e. A -. x [C.] y ) |
19 |
15 18
|
sylan2 |
|- ( ( A e. dom card /\ A. z ( ( z C_ A /\ [C.] Or z ) -> U. z e. A ) ) -> E. x e. A A. y e. A -. x [C.] y ) |
20 |
|
vex |
|- y e. _V |
21 |
20
|
brrpss |
|- ( x [C.] y <-> x C. y ) |
22 |
21
|
notbii |
|- ( -. x [C.] y <-> -. x C. y ) |
23 |
22
|
ralbii |
|- ( A. y e. A -. x [C.] y <-> A. y e. A -. x C. y ) |
24 |
23
|
rexbii |
|- ( E. x e. A A. y e. A -. x [C.] y <-> E. x e. A A. y e. A -. x C. y ) |
25 |
19 24
|
sylib |
|- ( ( A e. dom card /\ A. z ( ( z C_ A /\ [C.] Or z ) -> U. z e. A ) ) -> E. x e. A A. y e. A -. x C. y ) |