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	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ∈ Moore )

Proof

Step	Hyp	Ref	Expression
1		unisng	⊢ ( 𝐴 ∈ 𝑉 → ∪ { 𝐴 } = 𝐴 )
2		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
3	1 2	eqeltrd	⊢ ( 𝐴 ∈ 𝑉 → ∪ { 𝐴 } ∈ { 𝐴 } )
4		df-ne	⊢ ( 𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅ )
5		sssn	⊢ ( 𝑥 ⊆ { 𝐴 } ↔ ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) )
6		biorf	⊢ ( ¬ 𝑥 = ∅ → ( 𝑥 = { 𝐴 } ↔ ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ) )
7	6	biimpar	⊢ ( ( ¬ 𝑥 = ∅ ∧ ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ) → 𝑥 = { 𝐴 } )
8	4 5 7	syl2anb	⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ { 𝐴 } ) → 𝑥 = { 𝐴 } )
9		inteq	⊢ ( 𝑥 = { 𝐴 } → ∩ 𝑥 = ∩ { 𝐴 } )
10		intsng	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝐴 } = 𝐴 )
11		eqtr	⊢ ( ( ∩ 𝑥 = ∩ { 𝐴 } ∧ ∩ { 𝐴 } = 𝐴 ) → ∩ 𝑥 = 𝐴 )
12	11	ex	⊢ ( ∩ 𝑥 = ∩ { 𝐴 } → ( ∩ { 𝐴 } = 𝐴 → ∩ 𝑥 = 𝐴 ) )
13	9 10 12	syl2im	⊢ ( 𝑥 = { 𝐴 } → ( 𝐴 ∈ 𝑉 → ∩ 𝑥 = 𝐴 ) )
14		intex	⊢ ( 𝑥 ≠ ∅ ↔ ∩ 𝑥 ∈ V )
15		elsng	⊢ ( ∩ 𝑥 ∈ V → ( ∩ 𝑥 ∈ { 𝐴 } ↔ ∩ 𝑥 = 𝐴 ) )
16	14 15	sylbi	⊢ ( 𝑥 ≠ ∅ → ( ∩ 𝑥 ∈ { 𝐴 } ↔ ∩ 𝑥 = 𝐴 ) )
17	16	biimprd	⊢ ( 𝑥 ≠ ∅ → ( ∩ 𝑥 = 𝐴 → ∩ 𝑥 ∈ { 𝐴 } ) )
18	13 17	sylan9r	⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 = { 𝐴 } ) → ( 𝐴 ∈ 𝑉 → ∩ 𝑥 ∈ { 𝐴 } ) )
19	8 18	syldan	⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ { 𝐴 } ) → ( 𝐴 ∈ 𝑉 → ∩ 𝑥 ∈ { 𝐴 } ) )
20	19	ancoms	⊢ ( ( 𝑥 ⊆ { 𝐴 } ∧ 𝑥 ≠ ∅ ) → ( 𝐴 ∈ 𝑉 → ∩ 𝑥 ∈ { 𝐴 } ) )
21	20	impcom	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ⊆ { 𝐴 } ∧ 𝑥 ≠ ∅ ) ) → ∩ 𝑥 ∈ { 𝐴 } )
22	3 21	bj-ismooredr2	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ∈ Moore )