Theorem fsetsnprcnex

Description: The class of all functions from a (proper) singleton into a proper class B is not a set. (Contributed by AV, 13-Sep-2024)

	Ref	Expression
Assertion	fsetsnprcnex	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∉ V ) → { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } ∉ V )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } }
2		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ { ⟨ 𝑆 , 𝑥 ⟩ } ) = ( 𝑥 ∈ 𝐵 ↦ { ⟨ 𝑆 , 𝑥 ⟩ } )
3	1 2	fsetsnf1o	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑥 ∈ 𝐵 ↦ { ⟨ 𝑆 , 𝑥 ⟩ } ) : 𝐵 –1-1-onto→ { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } )
4		f1ovv	⊢ ( ( 𝑥 ∈ 𝐵 ↦ { ⟨ 𝑆 , 𝑥 ⟩ } ) : 𝐵 –1-1-onto→ { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } → ( 𝐵 ∈ V ↔ { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } ∈ V ) )
5	3 4	syl	⊢ ( 𝑆 ∈ 𝑉 → ( 𝐵 ∈ V ↔ { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } ∈ V ) )
6	5	notbid	⊢ ( 𝑆 ∈ 𝑉 → ( ¬ 𝐵 ∈ V ↔ ¬ { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } ∈ V ) )
7		df-nel	⊢ ( 𝐵 ∉ V ↔ ¬ 𝐵 ∈ V )
8		df-nel	⊢ ( { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } ∉ V ↔ ¬ { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } ∈ V )
9	6 7 8	3bitr4g	⊢ ( 𝑆 ∈ 𝑉 → ( 𝐵 ∉ V ↔ { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } ∉ V ) )
10	9	biimpa	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∉ V ) → { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } ∉ V )
11		fsetabsnop	⊢ ( 𝑆 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } )
12	11	adantr	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∉ V ) → { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } )
13		eqidd	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∉ V ) → V = V )
14	12 13	neleq12d	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∉ V ) → ( { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } ∉ V ↔ { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } ∉ V ) )
15	10 14	mpbird	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∉ V ) → { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } ∉ V )