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

Metamath Proof Explorer

Theorem uffix

Description: Lemma for fixufil and uffixfr . (Contributed by Mario Carneiro, 12-Dec-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion uffix 
|- ( ( X e. V /\ A e. X ) -> ( { { A } } e. ( fBas ` X ) /\ { x e. ~P X | A e. x } = ( X filGen { { A } } ) ) )

Proof

Step Hyp Ref Expression
1 snssi 
 |-  ( A e. X -> { A } C_ X )
2 snnzg 
 |-  ( A e. X -> { A } =/= (/) )
3 simpl 
 |-  ( ( X e. V /\ A e. X ) -> X e. V )
4 snfbas 
 |-  ( ( { A } C_ X /\ { A } =/= (/) /\ X e. V ) -> { { A } } e. ( fBas ` X ) )
5 1 2 3 4 syl2an23an 
 |-  ( ( X e. V /\ A e. X ) -> { { A } } e. ( fBas ` X ) )
6 velpw 
 |-  ( y e. ~P X <-> y C_ X )
7 6 a1i 
 |-  ( ( X e. V /\ A e. X ) -> ( y e. ~P X <-> y C_ X ) )
8 snex 
 |-  { A } e. _V
9 8 snid 
 |-  { A } e. { { A } }
10 snssi 
 |-  ( A e. y -> { A } C_ y )
11 sseq1 
 |-  ( x = { A } -> ( x C_ y <-> { A } C_ y ) )
12 11 rspcev 
 |-  ( ( { A } e. { { A } } /\ { A } C_ y ) -> E. x e. { { A } } x C_ y )
13 9 10 12 sylancr 
 |-  ( A e. y -> E. x e. { { A } } x C_ y )
14 intss1 
 |-  ( x e. { { A } } -> |^| { { A } } C_ x )
15 sstr2 
 |-  ( |^| { { A } } C_ x -> ( x C_ y -> |^| { { A } } C_ y ) )
16 14 15 syl 
 |-  ( x e. { { A } } -> ( x C_ y -> |^| { { A } } C_ y ) )
17 snidg 
 |-  ( A e. X -> A e. { A } )
18 17 adantl 
 |-  ( ( X e. V /\ A e. X ) -> A e. { A } )
19 8 intsn 
 |-  |^| { { A } } = { A }
20 18 19 eleqtrrdi 
 |-  ( ( X e. V /\ A e. X ) -> A e. |^| { { A } } )
21 ssel 
 |-  ( |^| { { A } } C_ y -> ( A e. |^| { { A } } -> A e. y ) )
22 20 21 syl5com 
 |-  ( ( X e. V /\ A e. X ) -> ( |^| { { A } } C_ y -> A e. y ) )
23 16 22 sylan9r 
 |-  ( ( ( X e. V /\ A e. X ) /\ x e. { { A } } ) -> ( x C_ y -> A e. y ) )
24 23 rexlimdva 
 |-  ( ( X e. V /\ A e. X ) -> ( E. x e. { { A } } x C_ y -> A e. y ) )
25 13 24 impbid2 
 |-  ( ( X e. V /\ A e. X ) -> ( A e. y <-> E. x e. { { A } } x C_ y ) )
26 7 25 anbi12d 
 |-  ( ( X e. V /\ A e. X ) -> ( ( y e. ~P X /\ A e. y ) <-> ( y C_ X /\ E. x e. { { A } } x C_ y ) ) )
27 eleq2w 
 |-  ( x = y -> ( A e. x <-> A e. y ) )
28 27 elrab 
 |-  ( y e. { x e. ~P X | A e. x } <-> ( y e. ~P X /\ A e. y ) )
29 28 a1i 
 |-  ( ( X e. V /\ A e. X ) -> ( y e. { x e. ~P X | A e. x } <-> ( y e. ~P X /\ A e. y ) ) )
30 elfg 
 |-  ( { { A } } e. ( fBas ` X ) -> ( y e. ( X filGen { { A } } ) <-> ( y C_ X /\ E. x e. { { A } } x C_ y ) ) )
31 5 30 syl 
 |-  ( ( X e. V /\ A e. X ) -> ( y e. ( X filGen { { A } } ) <-> ( y C_ X /\ E. x e. { { A } } x C_ y ) ) )
32 26 29 31 3bitr4d 
 |-  ( ( X e. V /\ A e. X ) -> ( y e. { x e. ~P X | A e. x } <-> y e. ( X filGen { { A } } ) ) )
33 32 eqrdv 
 |-  ( ( X e. V /\ A e. X ) -> { x e. ~P X | A e. x } = ( X filGen { { A } } ) )
34 5 33 jca 
 |-  ( ( X e. V /\ A e. X ) -> ( { { A } } e. ( fBas ` X ) /\ { x e. ~P X | A e. x } = ( X filGen { { A } } ) ) )