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 e. V -> { f | f : { S } --> B } = U_ b e. B { { <. S , b >. } } )

Proof

Step Hyp Ref Expression
1 fsn2g 
 |-  ( S e. V -> ( g : { S } --> B <-> ( ( g ` S ) e. B /\ g = { <. S , ( g ` S ) >. } ) ) )
2 simpl 
 |-  ( ( ( g ` S ) e. B /\ g = { <. S , ( g ` S ) >. } ) -> ( g ` S ) e. 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 ) e. B /\ g = { <. S , ( g ` S ) >. } ) /\ b = ( g ` S ) ) -> ( g = { <. S , b >. } <-> g = { <. S , ( g ` S ) >. } ) )
7 simpr 
 |-  ( ( ( g ` S ) e. B /\ g = { <. S , ( g ` S ) >. } ) -> g = { <. S , ( g ` S ) >. } )
8 2 6 7 rspcedvd 
 |-  ( ( ( g ` S ) e. B /\ g = { <. S , ( g ` S ) >. } ) -> E. b e. B g = { <. S , b >. } )
9 1 8 biimtrdi 
 |-  ( S e. V -> ( g : { S } --> B -> E. b e. B g = { <. S , b >. } ) )
10 simpl 
 |-  ( ( S e. V /\ b e. B ) -> S e. V )
11 simpr 
 |-  ( ( S e. V /\ b e. B ) -> b e. B )
12 10 11 fsnd 
 |-  ( ( S e. V /\ b e. B ) -> { <. S , b >. } : { S } --> B )
13 12 adantr 
 |-  ( ( ( S e. V /\ b e. B ) /\ g = { <. S , b >. } ) -> { <. S , b >. } : { S } --> B )
14 simpr 
 |-  ( ( ( S e. V /\ b e. B ) /\ g = { <. S , b >. } ) -> g = { <. S , b >. } )
15 14 feq1d 
 |-  ( ( ( S e. V /\ b e. B ) /\ g = { <. S , b >. } ) -> ( g : { S } --> B <-> { <. S , b >. } : { S } --> B ) )
16 13 15 mpbird 
 |-  ( ( ( S e. V /\ b e. B ) /\ g = { <. S , b >. } ) -> g : { S } --> B )
17 16 ex 
 |-  ( ( S e. V /\ b e. B ) -> ( g = { <. S , b >. } -> g : { S } --> B ) )
18 17 rexlimdva 
 |-  ( S e. V -> ( E. b e. B g = { <. S , b >. } -> g : { S } --> B ) )
19 9 18 impbid 
 |-  ( S e. V -> ( g : { S } --> B <-> E. b e. B g = { <. S , b >. } ) )
20 velsn 
 |-  ( g e. { { <. S , b >. } } <-> g = { <. S , b >. } )
21 20 bicomi 
 |-  ( g = { <. S , b >. } <-> g e. { { <. S , b >. } } )
22 21 rexbii 
 |-  ( E. b e. B g = { <. S , b >. } <-> E. b e. B g e. { { <. S , b >. } } )
23 19 22 bitrdi 
 |-  ( S e. V -> ( g : { S } --> B <-> E. b e. B g e. { { <. S , b >. } } ) )
24 vex 
 |-  g e. _V
25 feq1 
 |-  ( f = g -> ( f : { S } --> B <-> g : { S } --> B ) )
26 24 25 elab 
 |-  ( g e. { f | f : { S } --> B } <-> g : { S } --> B )
27 eliun 
 |-  ( g e. U_ b e. B { { <. S , b >. } } <-> E. b e. B g e. { { <. S , b >. } } )
28 23 26 27 3bitr4g 
 |-  ( S e. V -> ( g e. { f | f : { S } --> B } <-> g e. U_ b e. B { { <. S , b >. } } ) )
29 28 eqrdv 
 |-  ( S e. V -> { f | f : { S } --> B } = U_ b e. B { { <. S , b >. } } )