Theorem bj-snmoore

Description: A singleton is a Moore collection. See bj-snmooreb for a biconditional version. (Contributed by BJ, 10-Apr-2024)

	Ref	Expression
Assertion	bj-snmoore	|- ( A e. V -> { A } e. Moore_ )

Proof

Step	Hyp	Ref	Expression
1		unisng	|- ( A e. V -> U. { A } = A )
2		snidg	|- ( A e. V -> A e. { A } )
3	1 2	eqeltrd	|- ( A e. V -> U. { A } e. { A } )
4		df-ne	|- ( x =/= (/) <-> -. x = (/) )
5		sssn	|- ( x C_ { A } <-> ( x = (/) \/ x = { A } ) )
6		biorf	|- ( -. x = (/) -> ( x = { A } <-> ( x = (/) \/ x = { A } ) ) )
7	6	biimpar	|- ( ( -. x = (/) /\ ( x = (/) \/ x = { A } ) ) -> x = { A } )
8	4 5 7	syl2anb	|- ( ( x =/= (/) /\ x C_ { A } ) -> x = { A } )
9		inteq	|- ( x = { A } -> |^| x = |^| { A } )
10		intsng	|- ( A e. V -> |^| { A } = A )
11		eqtr	|- ( ( |^| x = |^| { A } /\ |^| { A } = A ) -> |^| x = A )
12	11	ex	|- ( |^| x = |^| { A } -> ( |^| { A } = A -> |^| x = A ) )
13	9 10 12	syl2im	|- ( x = { A } -> ( A e. V -> |^| x = A ) )
14		intex	|- ( x =/= (/) <-> |^| x e. _V )
15		elsng	|- ( |^| x e. _V -> ( |^| x e. { A } <-> |^| x = A ) )
16	14 15	sylbi	|- ( x =/= (/) -> ( |^| x e. { A } <-> |^| x = A ) )
17	16	biimprd	|- ( x =/= (/) -> ( |^| x = A -> |^| x e. { A } ) )
18	13 17	sylan9r	|- ( ( x =/= (/) /\ x = { A } ) -> ( A e. V -> |^| x e. { A } ) )
19	8 18	syldan	|- ( ( x =/= (/) /\ x C_ { A } ) -> ( A e. V -> |^| x e. { A } ) )
20	19	ancoms	|- ( ( x C_ { A } /\ x =/= (/) ) -> ( A e. V -> |^| x e. { A } ) )
21	20	impcom	|- ( ( A e. V /\ ( x C_ { A } /\ x =/= (/) ) ) -> |^| x e. { A } )
22	3 21	bj-ismooredr2	|- ( A e. V -> { A } e. Moore_ )