Theorem fsetsniunop

Description: The class of all functions from a (proper) singleton into B is the union of all the singletons of (proper) ordered pairs over the elements of B as second component. (Contributed by AV, 13-Sep-2024)

	Ref	Expression
Assertion	fsetsniunop	$$⊢S\in V\to \left\{f|f:\left\{S\right\}⟶B\right\}=\bigcup _{b\in B}\left\{\left\{⟨S,b⟩\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fsn2g	$$⊢S\in V\to \left(g:\left\{S\right\}⟶B\leftrightarrow \left(g\left(S\right)\in B\wedge g=\left\{⟨S,g\left(S\right)⟩\right\}\right)\right)$$
2		simpl	$$⊢\left(g\left(S\right)\in B\wedge g=\left\{⟨S,g\left(S\right)⟩\right\}\right)\to g\left(S\right)\in B$$
3		opeq2	$$⊢b=g\left(S\right)\to ⟨S,b⟩=⟨S,g\left(S\right)⟩$$
4	3	sneqd	$$⊢b=g\left(S\right)\to \left\{⟨S,b⟩\right\}=\left\{⟨S,g\left(S\right)⟩\right\}$$
5	4	eqeq2d	$$⊢b=g\left(S\right)\to \left(g=\left\{⟨S,b⟩\right\}\leftrightarrow g=\left\{⟨S,g\left(S\right)⟩\right\}\right)$$
6	5	adantl	$$⊢\left(\left(g\left(S\right)\in B\wedge g=\left\{⟨S,g\left(S\right)⟩\right\}\right)\wedge b=g\left(S\right)\right)\to \left(g=\left\{⟨S,b⟩\right\}\leftrightarrow g=\left\{⟨S,g\left(S\right)⟩\right\}\right)$$
7		simpr	$$⊢\left(g\left(S\right)\in B\wedge g=\left\{⟨S,g\left(S\right)⟩\right\}\right)\to g=\left\{⟨S,g\left(S\right)⟩\right\}$$
8	2 6 7	rspcedvd	$$⊢\left(g\left(S\right)\in B\wedge g=\left\{⟨S,g\left(S\right)⟩\right\}\right)\to \exists b\in Bg=\left\{⟨S,b⟩\right\}$$
9	1 8	biimtrdi	$$⊢S\in V\to \left(g:\left\{S\right\}⟶B\to \exists b\in Bg=\left\{⟨S,b⟩\right\}\right)$$
10		simpl	$$⊢\left(S\in V\wedge b\in B\right)\to S\in V$$
11		simpr	$$⊢\left(S\in V\wedge b\in B\right)\to b\in B$$
12	10 11	fsnd	$$⊢\left(S\in V\wedge b\in B\right)\to \left\{⟨S,b⟩\right\}:\left\{S\right\}⟶B$$
13	12	adantr	$$⊢\left(\left(S\in V\wedge b\in B\right)\wedge g=\left\{⟨S,b⟩\right\}\right)\to \left\{⟨S,b⟩\right\}:\left\{S\right\}⟶B$$
14		simpr	$$⊢\left(\left(S\in V\wedge b\in B\right)\wedge g=\left\{⟨S,b⟩\right\}\right)\to g=\left\{⟨S,b⟩\right\}$$
15	14	feq1d	$$⊢\left(\left(S\in V\wedge b\in B\right)\wedge g=\left\{⟨S,b⟩\right\}\right)\to \left(g:\left\{S\right\}⟶B\leftrightarrow \left\{⟨S,b⟩\right\}:\left\{S\right\}⟶B\right)$$
16	13 15	mpbird	$$⊢\left(\left(S\in V\wedge b\in B\right)\wedge g=\left\{⟨S,b⟩\right\}\right)\to g:\left\{S\right\}⟶B$$
17	16	ex	$$⊢\left(S\in V\wedge b\in B\right)\to \left(g=\left\{⟨S,b⟩\right\}\to g:\left\{S\right\}⟶B\right)$$
18	17	rexlimdva	$$⊢S\in V\to \left(\exists b\in Bg=\left\{⟨S,b⟩\right\}\to g:\left\{S\right\}⟶B\right)$$
19	9 18	impbid	$$⊢S\in V\to \left(g:\left\{S\right\}⟶B\leftrightarrow \exists b\in Bg=\left\{⟨S,b⟩\right\}\right)$$
20		velsn	$$⊢g\in \left\{\left\{⟨S,b⟩\right\}\right\}\leftrightarrow g=\left\{⟨S,b⟩\right\}$$
21	20	bicomi	$$⊢g=\left\{⟨S,b⟩\right\}\leftrightarrow g\in \left\{\left\{⟨S,b⟩\right\}\right\}$$
22	21	rexbii	$$⊢\exists b\in Bg=\left\{⟨S,b⟩\right\}\leftrightarrow \exists b\in Bg\in \left\{\left\{⟨S,b⟩\right\}\right\}$$
23	19 22	bitrdi	$$⊢S\in V\to \left(g:\left\{S\right\}⟶B\leftrightarrow \exists b\in Bg\in \left\{\left\{⟨S,b⟩\right\}\right\}\right)$$
24		vex	$$⊢g\in \mathrm{V}$$
25		feq1	$$⊢f=g\to \left(f:\left\{S\right\}⟶B\leftrightarrow g:\left\{S\right\}⟶B\right)$$
26	24 25	elab	$$⊢g\in \left\{f|f:\left\{S\right\}⟶B\right\}\leftrightarrow g:\left\{S\right\}⟶B$$
27		eliun	$$⊢g\in \bigcup _{b\in B}\left\{\left\{⟨S,b⟩\right\}\right\}\leftrightarrow \exists b\in Bg\in \left\{\left\{⟨S,b⟩\right\}\right\}$$
28	23 26 27	3bitr4g	$$⊢S\in V\to \left(g\in \left\{f|f:\left\{S\right\}⟶B\right\}\leftrightarrow g\in \bigcup _{b\in B}\left\{\left\{⟨S,b⟩\right\}\right\}\right)$$
29	28	eqrdv	$$⊢S\in V\to \left\{f|f:\left\{S\right\}⟶B\right\}=\bigcup _{b\in B}\left\{\left\{⟨S,b⟩\right\}\right\}$$