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 ( 𝑆 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } = ∪ 𝑏 ∈ 𝐵 { { ⟨ 𝑆 , 𝑏 ⟩ } } )

Proof

Step Hyp Ref Expression
1 fsn2g ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑔 : { 𝑆 } ⟶ 𝐵 ↔ ( ( 𝑔 ‘ 𝑆 ) ∈ 𝐵 ∧ 𝑔 = { ⟨ 𝑆 , ( 𝑔 ‘ 𝑆 ) ⟩ } ) ) )
2 simpl ⊢ ( ( ( 𝑔 ‘ 𝑆 ) ∈ 𝐵 ∧ 𝑔 = { ⟨ 𝑆 , ( 𝑔 ‘ 𝑆 ) ⟩ } ) → ( 𝑔 ‘ 𝑆 ) ∈ 𝐵 )
3 opeq2 ⊢ ( 𝑏 = ( 𝑔 ‘ 𝑆 ) → ⟨ 𝑆 , 𝑏 ⟩ = ⟨ 𝑆 , ( 𝑔 ‘ 𝑆 ) ⟩ )
4 3 sneqd ⊢ ( 𝑏 = ( 𝑔 ‘ 𝑆 ) → { ⟨ 𝑆 , 𝑏 ⟩ } = { ⟨ 𝑆 , ( 𝑔 ‘ 𝑆 ) ⟩ } )
5 4 eqeq2d ⊢ ( 𝑏 = ( 𝑔 ‘ 𝑆 ) → ( 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } ↔ 𝑔 = { ⟨ 𝑆 , ( 𝑔 ‘ 𝑆 ) ⟩ } ) )
6 5 adantl ⊢ ( ( ( ( 𝑔 ‘ 𝑆 ) ∈ 𝐵 ∧ 𝑔 = { ⟨ 𝑆 , ( 𝑔 ‘ 𝑆 ) ⟩ } ) ∧ 𝑏 = ( 𝑔 ‘ 𝑆 ) ) → ( 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } ↔ 𝑔 = { ⟨ 𝑆 , ( 𝑔 ‘ 𝑆 ) ⟩ } ) )
7 simpr ⊢ ( ( ( 𝑔 ‘ 𝑆 ) ∈ 𝐵 ∧ 𝑔 = { ⟨ 𝑆 , ( 𝑔 ‘ 𝑆 ) ⟩ } ) → 𝑔 = { ⟨ 𝑆 , ( 𝑔 ‘ 𝑆 ) ⟩ } )
8 2 6 7 rspcedvd ⊢ ( ( ( 𝑔 ‘ 𝑆 ) ∈ 𝐵 ∧ 𝑔 = { ⟨ 𝑆 , ( 𝑔 ‘ 𝑆 ) ⟩ } ) → ∃ 𝑏 ∈ 𝐵 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } )
9 1 8 syl6bi ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑔 : { 𝑆 } ⟶ 𝐵 → ∃ 𝑏 ∈ 𝐵 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } ) )
10 simpl ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵 ) → 𝑆 ∈ 𝑉 )
11 simpr ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
12 10 11 fsnd ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵 ) → { ⟨ 𝑆 , 𝑏 ⟩ } : { 𝑆 } ⟶ 𝐵 )
13 12 adantr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } ) → { ⟨ 𝑆 , 𝑏 ⟩ } : { 𝑆 } ⟶ 𝐵 )
14 simpr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } ) → 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } )
15 14 feq1d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } ) → ( 𝑔 : { 𝑆 } ⟶ 𝐵 ↔ { ⟨ 𝑆 , 𝑏 ⟩ } : { 𝑆 } ⟶ 𝐵 ) )
16 13 15 mpbird ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } ) → 𝑔 : { 𝑆 } ⟶ 𝐵 )
17 16 ex ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } → 𝑔 : { 𝑆 } ⟶ 𝐵 ) )
18 17 rexlimdva ⊢ ( 𝑆 ∈ 𝑉 → ( ∃ 𝑏 ∈ 𝐵 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } → 𝑔 : { 𝑆 } ⟶ 𝐵 ) )
19 9 18 impbid ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑔 : { 𝑆 } ⟶ 𝐵 ↔ ∃ 𝑏 ∈ 𝐵 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } ) )
20 velsn ⊢ ( 𝑔 ∈ { { ⟨ 𝑆 , 𝑏 ⟩ } } ↔ 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } )
21 20 bicomi ⊢ ( 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } ↔ 𝑔 ∈ { { ⟨ 𝑆 , 𝑏 ⟩ } } )
22 21 rexbii ⊢ ( ∃ 𝑏 ∈ 𝐵 𝑔 = { ⟨ 𝑆 , 𝑏 ⟩ } ↔ ∃ 𝑏 ∈ 𝐵 𝑔 ∈ { { ⟨ 𝑆 , 𝑏 ⟩ } } )
23 19 22 bitrdi ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑔 : { 𝑆 } ⟶ 𝐵 ↔ ∃ 𝑏 ∈ 𝐵 𝑔 ∈ { { ⟨ 𝑆 , 𝑏 ⟩ } } ) )
24 vex ⊢ 𝑔 ∈ V
25 feq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 : { 𝑆 } ⟶ 𝐵 ↔ 𝑔 : { 𝑆 } ⟶ 𝐵 ) )
26 24 25 elab ⊢ ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } ↔ 𝑔 : { 𝑆 } ⟶ 𝐵 )
27 eliun ⊢ ( 𝑔 ∈ ∪ 𝑏 ∈ 𝐵 { { ⟨ 𝑆 , 𝑏 ⟩ } } ↔ ∃ 𝑏 ∈ 𝐵 𝑔 ∈ { { ⟨ 𝑆 , 𝑏 ⟩ } } )
28 23 26 27 3bitr4g ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } ↔ 𝑔 ∈ ∪ 𝑏 ∈ 𝐵 { { ⟨ 𝑆 , 𝑏 ⟩ } } ) )
29 28 eqrdv ⊢ ( 𝑆 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } = ∪ 𝑏 ∈ 𝐵 { { ⟨ 𝑆 , 𝑏 ⟩ } } )