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