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 ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) ∧ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } = ( 𝑋 filGen { { 𝐴 } } ) ) )

Proof

Step Hyp Ref Expression
1 snssi ⊢ ( 𝐴 ∈ 𝑋 → { 𝐴 } ⊆ 𝑋 )
2 snnzg ⊢ ( 𝐴 ∈ 𝑋 → { 𝐴 } ≠ ∅ )
3 simpl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → 𝑋 ∈ 𝑉 )
4 snfbas ⊢ ( ( { 𝐴 } ⊆ 𝑋 ∧ { 𝐴 } ≠ ∅ ∧ 𝑋 ∈ 𝑉 ) → { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) )
5 1 2 3 4 syl2an23an ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) )
6 velpw ⊢ ( 𝑦 ∈ 𝒫 𝑋 ↔ 𝑦 ⊆ 𝑋 )
7 6 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑦 ∈ 𝒫 𝑋 ↔ 𝑦 ⊆ 𝑋 ) )
8 snex ⊢ { 𝐴 } ∈ V
9 8 snid ⊢ { 𝐴 } ∈ { { 𝐴 } }
10 snssi ⊢ ( 𝐴 ∈ 𝑦 → { 𝐴 } ⊆ 𝑦 )
11 sseq1 ⊢ ( 𝑥 = { 𝐴 } → ( 𝑥 ⊆ 𝑦 ↔ { 𝐴 } ⊆ 𝑦 ) )
12 11 rspcev ⊢ ( ( { 𝐴 } ∈ { { 𝐴 } } ∧ { 𝐴 } ⊆ 𝑦 ) → ∃ 𝑥 ∈ { { 𝐴 } } 𝑥 ⊆ 𝑦 )
13 9 10 12 sylancr ⊢ ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ { { 𝐴 } } 𝑥 ⊆ 𝑦 )
14 intss1 ⊢ ( 𝑥 ∈ { { 𝐴 } } → ∩ { { 𝐴 } } ⊆ 𝑥 )
15 sstr2 ⊢ ( ∩ { { 𝐴 } } ⊆ 𝑥 → ( 𝑥 ⊆ 𝑦 → ∩ { { 𝐴 } } ⊆ 𝑦 ) )
16 14 15 syl ⊢ ( 𝑥 ∈ { { 𝐴 } } → ( 𝑥 ⊆ 𝑦 → ∩ { { 𝐴 } } ⊆ 𝑦 ) )
17 snidg ⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ { 𝐴 } )
18 17 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ { 𝐴 } )
19 8 intsn ⊢ ∩ { { 𝐴 } } = { 𝐴 }
20 18 19 eleqtrrdi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ∩ { { 𝐴 } } )
21 ssel ⊢ ( ∩ { { 𝐴 } } ⊆ 𝑦 → ( 𝐴 ∈ ∩ { { 𝐴 } } → 𝐴 ∈ 𝑦 ) )
22 20 21 syl5com ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( ∩ { { 𝐴 } } ⊆ 𝑦 → 𝐴 ∈ 𝑦 ) )
23 16 22 sylan9r ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ { { 𝐴 } } ) → ( 𝑥 ⊆ 𝑦 → 𝐴 ∈ 𝑦 ) )
24 23 rexlimdva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ { { 𝐴 } } 𝑥 ⊆ 𝑦 → 𝐴 ∈ 𝑦 ) )
25 13 24 impbid2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑦 ↔ ∃ 𝑥 ∈ { { 𝐴 } } 𝑥 ⊆ 𝑦 ) )
26 7 25 anbi12d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ↔ ( 𝑦 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ { { 𝐴 } } 𝑥 ⊆ 𝑦 ) ) )
27 eleq2w ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) )
28 27 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) )
29 28 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ) )
30 elfg ⊢ ( { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) → ( 𝑦 ∈ ( 𝑋 filGen { { 𝐴 } } ) ↔ ( 𝑦 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ { { 𝐴 } } 𝑥 ⊆ 𝑦 ) ) )
31 5 30 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑦 ∈ ( 𝑋 filGen { { 𝐴 } } ) ↔ ( 𝑦 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ { { 𝐴 } } 𝑥 ⊆ 𝑦 ) ) )
32 26 29 31 3bitr4d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ↔ 𝑦 ∈ ( 𝑋 filGen { { 𝐴 } } ) ) )
33 32 eqrdv ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } = ( 𝑋 filGen { { 𝐴 } } ) )
34 5 33 jca ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) ∧ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } = ( 𝑋 filGen { { 𝐴 } } ) ) )