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

Metamath Proof Explorer

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 ) ) }