Description: An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | ixp0x | |- X_ x e. (/) A = { (/) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfixp | |- X_ x e. (/) A = { f | ( f Fn (/) /\ A. x e. (/) ( f ` x ) e. A ) } |
|
2 | velsn | |- ( f e. { (/) } <-> f = (/) ) |
|
3 | fn0 | |- ( f Fn (/) <-> f = (/) ) |
|
4 | ral0 | |- A. x e. (/) ( f ` x ) e. A |
|
5 | 4 | biantru | |- ( f Fn (/) <-> ( f Fn (/) /\ A. x e. (/) ( f ` x ) e. A ) ) |
6 | 2 3 5 | 3bitr2i | |- ( f e. { (/) } <-> ( f Fn (/) /\ A. x e. (/) ( f ` x ) e. A ) ) |
7 | 6 | abbi2i | |- { (/) } = { f | ( f Fn (/) /\ A. x e. (/) ( f ` x ) e. A ) } |
8 | 1 7 | eqtr4i | |- X_ x e. (/) A = { (/) } |