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 = X filGen A

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 ∈ A x ⊆ y
13 9 10 12 sylancr ⊢ A ∈ y → ∃ x ∈ A x ⊆ 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 ∈ A x ⊆ y → A ∈ y
25 13 24 impbid2 ⊢ X ∈ V ∧ A ∈ X → A ∈ y ↔ ∃ x ∈ A x ⊆ y
26 7 25 anbi12d ⊢ X ∈ V ∧ A ∈ X → y ∈ 𝒫 X ∧ A ∈ y ↔ y ⊆ X ∧ ∃ x ∈ A x ⊆ 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 ∈ X filGen A ↔ y ⊆ X ∧ ∃ x ∈ A x ⊆ y
31 5 30 syl ⊢ X ∈ V ∧ A ∈ X → y ∈ X filGen A ↔ y ⊆ X ∧ ∃ x ∈ A x ⊆ y
32 26 29 31 3bitr4d ⊢ X ∈ V ∧ A ∈ X → y ∈ x ∈ 𝒫 X | A ∈ x ↔ y ∈ X filGen A
33 32 eqrdv ⊢ X ∈ V ∧ A ∈ X → x ∈ 𝒫 X | A ∈ x = X filGen A
34 5 33 jca ⊢ X ∈ V ∧ A ∈ X → A ∈ fBas ⁡ X ∧ x ∈ 𝒫 X | A ∈ x = X filGen A