Metamath Proof Explorer

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 ∈ V → f | f : S ⟶ B = ⋃ b ∈ B S b

Proof

Step Hyp Ref Expression
1 fsn2g ⊢ S ∈ V → g : S ⟶ B ↔ g ⁡ S ∈ B ∧ g = S g ⁡ S
2 simpl ⊢ g ⁡ S ∈ B ∧ g = S g ⁡ S → g ⁡ S ∈ B
3 opeq2 ⊢ b = g ⁡ S → S b = S g ⁡ S
4 3 sneqd ⊢ b = g ⁡ S → S b = S g ⁡ S
5 4 eqeq2d ⊢ b = g ⁡ S → g = S b ↔ g = S g ⁡ S
6 5 adantl ⊢ g ⁡ S ∈ B ∧ g = S g ⁡ S ∧ b = g ⁡ S → g = S b ↔ g = S g ⁡ S
7 simpr ⊢ g ⁡ S ∈ B ∧ g = S g ⁡ S → g = S g ⁡ S
8 2 6 7 rspcedvd ⊢ g ⁡ S ∈ B ∧ g = S g ⁡ S → ∃ b ∈ B g = S b
9 1 8 syl6bi ⊢ S ∈ V → g : S ⟶ B → ∃ b ∈ B g = S b
10 simpl ⊢ S ∈ V ∧ b ∈ B → S ∈ V
11 simpr ⊢ S ∈ V ∧ b ∈ B → b ∈ B
12 10 11 fsnd ⊢ S ∈ V ∧ b ∈ B → S b : S ⟶ B
13 12 adantr ⊢ S ∈ V ∧ b ∈ B ∧ g = S b → S b : S ⟶ B
14 simpr ⊢ S ∈ V ∧ b ∈ B ∧ g = S b → g = S b
15 14 feq1d ⊢ S ∈ V ∧ b ∈ B ∧ g = S b → g : S ⟶ B ↔ S b : S ⟶ B
16 13 15 mpbird ⊢ S ∈ V ∧ b ∈ B ∧ g = S b → g : S ⟶ B
17 16 ex ⊢ S ∈ V ∧ b ∈ B → g = S b → g : S ⟶ B
18 17 rexlimdva ⊢ S ∈ V → ∃ b ∈ B g = S b → g : S ⟶ B
19 9 18 impbid ⊢ S ∈ V → g : S ⟶ B ↔ ∃ b ∈ B g = S b
20 velsn ⊢ g ∈ S b ↔ g = S b
21 20 bicomi ⊢ g = S b ↔ g ∈ S b
22 21 rexbii ⊢ ∃ b ∈ B g = S b ↔ ∃ b ∈ B g ∈ S b
23 19 22 bitrdi ⊢ S ∈ V → g : S ⟶ B ↔ ∃ b ∈ B g ∈ S b
24 vex ⊢ g ∈ V
25 feq1 ⊢ f = g → f : S ⟶ B ↔ g : S ⟶ B
26 24 25 elab ⊢ g ∈ f | f : S ⟶ B ↔ g : S ⟶ B
27 eliun ⊢ g ∈ ⋃ b ∈ B S b ↔ ∃ b ∈ B g ∈ S b
28 23 26 27 3bitr4g ⊢ S ∈ V → g ∈ f | f : S ⟶ B ↔ g ∈ ⋃ b ∈ B S b
29 28 eqrdv ⊢ S ∈ V → f | f : S ⟶ B = ⋃ b ∈ B S b