This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbagsn ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝐾 , 1 , 0 ) ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 psrbag0.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 ) ) ∈ 𝐷 )