Metamath Proof Explorer


Theorem psrbagsn

Description: A singleton bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015)

Ref Expression
Hypothesis psrbag0.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbagsn ( 𝐼𝑉 → ( 𝑥𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 psrbag0.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 1nn0 1 ∈ ℕ0
3 0nn0 0 ∈ ℕ0
4 2 3 ifcli if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ0
5 4 a1i ( ( ⊤ ∧ 𝑥𝐼 ) → if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ0 )
6 5 fmpttd ( ⊤ → ( 𝑥𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) : 𝐼 ⟶ ℕ0 )
7 6 mptru ( 𝑥𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) : 𝐼 ⟶ ℕ0
8 eqid ( 𝑥𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) = ( 𝑥𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) )
9 8 mptpreima ( ( 𝑥𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) “ ℕ ) = { 𝑥𝐼 ∣ if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ }
10 snfi { 𝐾 } ∈ Fin
11 inss1 ( { 𝑥𝑥 = 𝐾 } ∩ 𝐼 ) ⊆ { 𝑥𝑥 = 𝐾 }
12 dfrab2 { 𝑥𝐼𝑥 = 𝐾 } = ( { 𝑥𝑥 = 𝐾 } ∩ 𝐼 )
13 df-sn { 𝐾 } = { 𝑥𝑥 = 𝐾 }
14 11 12 13 3sstr4i { 𝑥𝐼𝑥 = 𝐾 } ⊆ { 𝐾 }
15 ssfi ( ( { 𝐾 } ∈ Fin ∧ { 𝑥𝐼𝑥 = 𝐾 } ⊆ { 𝐾 } ) → { 𝑥𝐼𝑥 = 𝐾 } ∈ Fin )
16 10 14 15 mp2an { 𝑥𝐼𝑥 = 𝐾 } ∈ Fin
17 0nnn ¬ 0 ∈ ℕ
18 iffalse ( ¬ 𝑥 = 𝐾 → if ( 𝑥 = 𝐾 , 1 , 0 ) = 0 )
19 18 eleq1d ( ¬ 𝑥 = 𝐾 → ( if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ ↔ 0 ∈ ℕ ) )
20 17 19 mtbiri ( ¬ 𝑥 = 𝐾 → ¬ if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ )
21 20 con4i ( if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ → 𝑥 = 𝐾 )
22 21 a1i ( 𝑥𝐼 → ( if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ → 𝑥 = 𝐾 ) )
23 22 ss2rabi { 𝑥𝐼 ∣ if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ } ⊆ { 𝑥𝐼𝑥 = 𝐾 }
24 ssfi ( ( { 𝑥𝐼𝑥 = 𝐾 } ∈ Fin ∧ { 𝑥𝐼 ∣ if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ } ⊆ { 𝑥𝐼𝑥 = 𝐾 } ) → { 𝑥𝐼 ∣ if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ } ∈ Fin )
25 16 23 24 mp2an { 𝑥𝐼 ∣ if ( 𝑥 = 𝐾 , 1 , 0 ) ∈ ℕ } ∈ Fin
26 9 25 eqeltri ( ( 𝑥𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) “ ℕ ) ∈ Fin
27 7 26 pm3.2i ( ( 𝑥𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) : 𝐼 ⟶ ℕ0 ∧ ( ( 𝑥𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) “ ℕ ) ∈ Fin )
28 1 psrbag ( 𝐼𝑉 → ( ( 𝑥𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) ∈ 𝐷 ↔ ( ( 𝑥𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) : 𝐼 ⟶ ℕ0 ∧ ( ( 𝑥𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) “ ℕ ) ∈ Fin ) ) )
29 27 28 mpbiri ( 𝐼𝑉 → ( 𝑥𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) ∈ 𝐷 )