Theorem marypha2lem2

Description: Lemma for marypha2 . Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015)

	Ref	Expression
Hypothesis	marypha2lem.t	|- T = U_ x e. A ( { x } X. ( F ` x ) )
Assertion	marypha2lem2	|- T = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }

Proof

Step	Hyp	Ref	Expression
1		marypha2lem.t	|- T = U_ x e. A ( { x } X. ( F ` x ) )
2		sneq	|- ( x = z -> { x } = { z } )
3		fveq2	|- ( x = z -> ( F ` x ) = ( F ` z ) )
4	2 3	xpeq12d	|- ( x = z -> ( { x } X. ( F ` x ) ) = ( { z } X. ( F ` z ) ) )
5	4	cbviunv	|- U_ x e. A ( { x } X. ( F ` x ) ) = U_ z e. A ( { z } X. ( F ` z ) )
6		df-xp	|- ( { z } X. ( F ` z ) ) = { <. x , y >. | ( x e. { z } /\ y e. ( F ` z ) ) }
7	6	a1i	|- ( z e. A -> ( { z } X. ( F ` z ) ) = { <. x , y >. | ( x e. { z } /\ y e. ( F ` z ) ) } )
8	7	iuneq2i	|- U_ z e. A ( { z } X. ( F ` z ) ) = U_ z e. A { <. x , y >. | ( x e. { z } /\ y e. ( F ` z ) ) }
9		iunopab	|- U_ z e. A { <. x , y >. | ( x e. { z } /\ y e. ( F ` z ) ) } = { <. x , y >. | E. z e. A ( x e. { z } /\ y e. ( F ` z ) ) }
10		velsn	|- ( x e. { z } <-> x = z )
11		equcom	|- ( x = z <-> z = x )
12	10 11	bitri	|- ( x e. { z } <-> z = x )
13	12	anbi1i	|- ( ( x e. { z } /\ y e. ( F ` z ) ) <-> ( z = x /\ y e. ( F ` z ) ) )
14	13	rexbii	|- ( E. z e. A ( x e. { z } /\ y e. ( F ` z ) ) <-> E. z e. A ( z = x /\ y e. ( F ` z ) ) )
15		fveq2	|- ( z = x -> ( F ` z ) = ( F ` x ) )
16	15	eleq2d	|- ( z = x -> ( y e. ( F ` z ) <-> y e. ( F ` x ) ) )
17	16	ceqsrexbv	|- ( E. z e. A ( z = x /\ y e. ( F ` z ) ) <-> ( x e. A /\ y e. ( F ` x ) ) )
18	14 17	bitri	|- ( E. z e. A ( x e. { z } /\ y e. ( F ` z ) ) <-> ( x e. A /\ y e. ( F ` x ) ) )
19	18	opabbii	|- { <. x , y >. | E. z e. A ( x e. { z } /\ y e. ( F ` z ) ) } = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }
20	8 9 19	3eqtri	|- U_ z e. A ( { z } X. ( F ` z ) ) = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }
21	1 5 20	3eqtri	|- T = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }