Theorem dmres

Description: The domain of a restriction. Exercise 14 of TakeutiZaring p. 25. (Contributed by NM, 1-Aug-1994)

	Ref	Expression
Assertion	dmres	|- dom ( A |` B ) = ( B i^i dom A )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	eldm2	|- ( x e. dom ( A |` B ) <-> E. y <. x , y >. e. ( A |` B ) )
3		19.42v	|- ( E. y ( x e. B /\ <. x , y >. e. A ) <-> ( x e. B /\ E. y <. x , y >. e. A ) )
4		vex	|- y e. _V
5	4	opelresi	|- ( <. x , y >. e. ( A |` B ) <-> ( x e. B /\ <. x , y >. e. A ) )
6	5	exbii	|- ( E. y <. x , y >. e. ( A |` B ) <-> E. y ( x e. B /\ <. x , y >. e. A ) )
7	1	eldm2	|- ( x e. dom A <-> E. y <. x , y >. e. A )
8	7	anbi2i	|- ( ( x e. B /\ x e. dom A ) <-> ( x e. B /\ E. y <. x , y >. e. A ) )
9	3 6 8	3bitr4i	|- ( E. y <. x , y >. e. ( A |` B ) <-> ( x e. B /\ x e. dom A ) )
10	2 9	bitr2i	|- ( ( x e. B /\ x e. dom A ) <-> x e. dom ( A |` B ) )
11	10	ineqri	|- ( B i^i dom A ) = dom ( A |` B )
12	11	eqcomi	|- dom ( A |` B ) = ( B i^i dom A )