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∈V∧A∈X→A∈fBas⁡X∧x∈𝒫X|A∈x=XfilGenA

Proof

Step Hyp Ref Expression
1 snssi ⊢A∈X→A⊆X
2 snnzg ⊢A∈X→A≠∅
3 simpl ⊢X∈V∧A∈X→X∈V
4 snfbas ⊢A⊆X∧A≠∅∧X∈V→A∈fBas⁡X
5 1 2 3 4 syl2an23an ⊢X∈V∧A∈X→A∈fBas⁡X
6 velpw ⊢y∈𝒫X↔y⊆X
7 6 a1i ⊢X∈V∧A∈X→y∈𝒫X↔y⊆X
8 snex ⊢A∈V
9 8 snid ⊢A∈A
10 snssi ⊢A∈y→A⊆y
11 sseq1 ⊢x=A→x⊆y↔A⊆y
12 11 rspcev ⊢A∈A∧A⊆y→∃x∈Ax⊆y
13 9 10 12 sylancr ⊢A∈y→∃x∈Ax⊆y
14 intss1 ⊢x∈A→⋂A⊆x
15 sstr2 ⊢⋂A⊆x→x⊆y→⋂A⊆y
16 14 15 syl ⊢x∈A→x⊆y→⋂A⊆y
17 snidg ⊢A∈X→A∈A
18 17 adantl ⊢X∈V∧A∈X→A∈A
19 8 intsn ⊢⋂A=A
20 18 19 eleqtrrdi ⊢X∈V∧A∈X→A∈⋂A
21 ssel ⊢⋂A⊆y→A∈⋂A→A∈y
22 20 21 syl5com ⊢X∈V∧A∈X→⋂A⊆y→A∈y
23 16 22 sylan9r ⊢X∈V∧A∈X∧x∈A→x⊆y→A∈y
24 23 rexlimdva ⊢X∈V∧A∈X→∃x∈Ax⊆y→A∈y
25 13 24 impbid2 ⊢X∈V∧A∈X→A∈y↔∃x∈Ax⊆y
26 7 25 anbi12d ⊢X∈V∧A∈X→y∈𝒫X∧A∈y↔y⊆X∧∃x∈Ax⊆y
27 eleq2w ⊢x=y→A∈x↔A∈y
28 27 elrab ⊢y∈x∈𝒫X|A∈x↔y∈𝒫X∧A∈y
29 28 a1i ⊢X∈V∧A∈X→y∈x∈𝒫X|A∈x↔y∈𝒫X∧A∈y
30 elfg ⊢A∈fBas⁡X→y∈XfilGenA↔y⊆X∧∃x∈Ax⊆y
31 5 30 syl ⊢X∈V∧A∈X→y∈XfilGenA↔y⊆X∧∃x∈Ax⊆y
32 26 29 31 3bitr4d ⊢X∈V∧A∈X→y∈x∈𝒫X|A∈x↔y∈XfilGenA
33 32 eqrdv ⊢X∈V∧A∈X→x∈𝒫X|A∈x=XfilGenA
34 5 33 jca ⊢X∈V∧A∈X→A∈fBas⁡X∧x∈𝒫X|A∈x=XfilGenA