Description: A cartesian product of proper-class many sets is empty, because any function in the cartesian product has to be a set with domain A , which is not possible for a proper class domain. (Contributed by Mario Carneiro, 25-Jan-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ixpprc | |- ( -. A e. _V -> X_ x e. A B = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | neq0 | |- ( -. X_ x e. A B = (/) <-> E. f f e. X_ x e. A B ) |
|
| 2 | ixpfn | |- ( f e. X_ x e. A B -> f Fn A ) |
|
| 3 | fndm | |- ( f Fn A -> dom f = A ) |
|
| 4 | vex | |- f e. _V |
|
| 5 | 4 | dmex | |- dom f e. _V |
| 6 | 3 5 | eqeltrrdi | |- ( f Fn A -> A e. _V ) |
| 7 | 2 6 | syl | |- ( f e. X_ x e. A B -> A e. _V ) |
| 8 | 7 | exlimiv | |- ( E. f f e. X_ x e. A B -> A e. _V ) |
| 9 | 1 8 | sylbi | |- ( -. X_ x e. A B = (/) -> A e. _V ) |
| 10 | 9 | con1i | |- ( -. A e. _V -> X_ x e. A B = (/) ) |