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