Metamath Proof Explorer

Theorem dfac5lem1

Description: Lemma for dfac5 . (Contributed by NM, 12-Apr-2004)

Ref Expression
Assertion dfac5lem1 
|- ( E! v v e. ( ( { w } X. w ) i^i y ) <-> E! g ( g e. w /\ <. w , g >. e. y ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( v e. ( ( { w } X. w ) i^i y ) <-> ( v e. ( { w } X. w ) /\ v e. y ) )
2 elxp 
 |-  ( v e. ( { w } X. w ) <-> E. t E. g ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) )
3 excom 
 |-  ( E. t E. g ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) <-> E. g E. t ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) )
4 2 3 bitri 
 |-  ( v e. ( { w } X. w ) <-> E. g E. t ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) )
5 4 anbi1i 
 |-  ( ( v e. ( { w } X. w ) /\ v e. y ) <-> ( E. g E. t ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) )
6 19.41vv 
 |-  ( E. g E. t ( ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> ( E. g E. t ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) )
7 an32 
 |-  ( ( ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> ( ( v = <. t , g >. /\ v e. y ) /\ ( t e. { w } /\ g e. w ) ) )
8 eleq1 
 |-  ( v = <. t , g >. -> ( v e. y <-> <. t , g >. e. y ) )
9 8 pm5.32i 
 |-  ( ( v = <. t , g >. /\ v e. y ) <-> ( v = <. t , g >. /\ <. t , g >. e. y ) )
10 velsn 
 |-  ( t e. { w } <-> t = w )
11 10 anbi1i 
 |-  ( ( t e. { w } /\ g e. w ) <-> ( t = w /\ g e. w ) )
12 9 11 anbi12i 
 |-  ( ( ( v = <. t , g >. /\ v e. y ) /\ ( t e. { w } /\ g e. w ) ) <-> ( ( v = <. t , g >. /\ <. t , g >. e. y ) /\ ( t = w /\ g e. w ) ) )
13 an4 
 |-  ( ( ( v = <. t , g >. /\ <. t , g >. e. y ) /\ ( t = w /\ g e. w ) ) <-> ( ( v = <. t , g >. /\ t = w ) /\ ( <. t , g >. e. y /\ g e. w ) ) )
14 ancom 
 |-  ( ( v = <. t , g >. /\ t = w ) <-> ( t = w /\ v = <. t , g >. ) )
15 ancom 
 |-  ( ( <. t , g >. e. y /\ g e. w ) <-> ( g e. w /\ <. t , g >. e. y ) )
16 14 15 anbi12i 
 |-  ( ( ( v = <. t , g >. /\ t = w ) /\ ( <. t , g >. e. y /\ g e. w ) ) <-> ( ( t = w /\ v = <. t , g >. ) /\ ( g e. w /\ <. t , g >. e. y ) ) )
17 anass 
 |-  ( ( ( t = w /\ v = <. t , g >. ) /\ ( g e. w /\ <. t , g >. e. y ) ) <-> ( t = w /\ ( v = <. t , g >. /\ ( g e. w /\ <. t , g >. e. y ) ) ) )
18 13 16 17 3bitri 
 |-  ( ( ( v = <. t , g >. /\ <. t , g >. e. y ) /\ ( t = w /\ g e. w ) ) <-> ( t = w /\ ( v = <. t , g >. /\ ( g e. w /\ <. t , g >. e. y ) ) ) )
19 7 12 18 3bitri 
 |-  ( ( ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> ( t = w /\ ( v = <. t , g >. /\ ( g e. w /\ <. t , g >. e. y ) ) ) )
20 19 exbii 
 |-  ( E. t ( ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> E. t ( t = w /\ ( v = <. t , g >. /\ ( g e. w /\ <. t , g >. e. y ) ) ) )
21 opeq1 
 |-  ( t = w -> <. t , g >. = <. w , g >. )
22 21 eqeq2d 
 |-  ( t = w -> ( v = <. t , g >. <-> v = <. w , g >. ) )
23 21 eleq1d 
 |-  ( t = w -> ( <. t , g >. e. y <-> <. w , g >. e. y ) )
24 23 anbi2d 
 |-  ( t = w -> ( ( g e. w /\ <. t , g >. e. y ) <-> ( g e. w /\ <. w , g >. e. y ) ) )
25 22 24 anbi12d 
 |-  ( t = w -> ( ( v = <. t , g >. /\ ( g e. w /\ <. t , g >. e. y ) ) <-> ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) ) )
26 25 equsexvw 
 |-  ( E. t ( t = w /\ ( v = <. t , g >. /\ ( g e. w /\ <. t , g >. e. y ) ) ) <-> ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) )
27 20 26 bitri 
 |-  ( E. t ( ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) )
28 27 exbii 
 |-  ( E. g E. t ( ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> E. g ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) )
29 6 28 bitr3i 
 |-  ( ( E. g E. t ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> E. g ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) )
30 1 5 29 3bitri 
 |-  ( v e. ( ( { w } X. w ) i^i y ) <-> E. g ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) )
31 30 eubii 
 |-  ( E! v v e. ( ( { w } X. w ) i^i y ) <-> E! v E. g ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) )
32 vex 
 |-  w e. _V
33 32 euop2 
 |-  ( E! v E. g ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) <-> E! g ( g e. w /\ <. w , g >. e. y ) )
34 31 33 bitri 
 |-  ( E! v v e. ( ( { w } X. w ) i^i y ) <-> E! g ( g e. w /\ <. w , g >. e. y ) )