This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ixpin

Description: The intersection of two infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015)

		Ref	Expression
	Assertion	ixpin	\|- X_ x e. A ( B i^i C ) = ( X_ x e. A B i^i X_ x e. A C )

Proof

Step	Hyp	Ref	Expression
1		anandi	\|- ( ( f Fn A /\ ( A. x e. A ( f ` x ) e. B /\ A. x e. A ( f ` x ) e. C ) ) <-> ( ( f Fn A /\ A. x e. A ( f ` x ) e. B ) /\ ( f Fn A /\ A. x e. A ( f ` x ) e. C ) ) )
2		elin	\|- ( ( f ` x ) e. ( B i^i C ) <-> ( ( f ` x ) e. B /\ ( f ` x ) e. C ) )
3	2	ralbii	\|- ( A. x e. A ( f ` x ) e. ( B i^i C ) <-> A. x e. A ( ( f ` x ) e. B /\ ( f ` x ) e. C ) )
4		r19.26	\|- ( A. x e. A ( ( f ` x ) e. B /\ ( f ` x ) e. C ) <-> ( A. x e. A ( f ` x ) e. B /\ A. x e. A ( f ` x ) e. C ) )
5	3 4	bitri	\|- ( A. x e. A ( f ` x ) e. ( B i^i C ) <-> ( A. x e. A ( f ` x ) e. B /\ A. x e. A ( f ` x ) e. C ) )
6	5	anbi2i	\|- ( ( f Fn A /\ A. x e. A ( f ` x ) e. ( B i^i C ) ) <-> ( f Fn A /\ ( A. x e. A ( f ` x ) e. B /\ A. x e. A ( f ` x ) e. C ) ) )
7		vex	\|- f e. _V
8	7	elixp	\|- ( f e. X_ x e. A B <-> ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
9	7	elixp	\|- ( f e. X_ x e. A C <-> ( f Fn A /\ A. x e. A ( f ` x ) e. C ) )
10	8 9	anbi12i	\|- ( ( f e. X_ x e. A B /\ f e. X_ x e. A C ) <-> ( ( f Fn A /\ A. x e. A ( f ` x ) e. B ) /\ ( f Fn A /\ A. x e. A ( f ` x ) e. C ) ) )
11	1 6 10	3bitr4i	\|- ( ( f Fn A /\ A. x e. A ( f ` x ) e. ( B i^i C ) ) <-> ( f e. X_ x e. A B /\ f e. X_ x e. A C ) )
12	7	elixp	\|- ( f e. X_ x e. A ( B i^i C ) <-> ( f Fn A /\ A. x e. A ( f ` x ) e. ( B i^i C ) ) )
13		elin	\|- ( f e. ( X_ x e. A B i^i X_ x e. A C ) <-> ( f e. X_ x e. A B /\ f e. X_ x e. A C ) )
14	11 12 13	3bitr4i	\|- ( f e. X_ x e. A ( B i^i C ) <-> f e. ( X_ x e. A B i^i X_ x e. A C ) )
15	14	eqriv	\|- X_ x e. A ( B i^i C ) = ( X_ x e. A B i^i X_ x e. A C )