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

Metamath Proof Explorer

Theorem psrbag0

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

Ref Expression
Hypothesis psrbag0.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbag0 ( 𝐼 ∈ 𝑉 → ( 𝐼 × { 0 } ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 psrbag0.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2 0nn0 ⊢ 0 ∈ ℕ0
3 2 fconst6 ⊢ ( 𝐼 × { 0 } ) : 𝐼 ⟶ ℕ0
4 c0ex ⊢ 0 ∈ V
5 4 fconst ⊢ ( 𝐼 × { 0 } ) : 𝐼 ⟶ { 0 }
6 incom ⊢ ( { 0 } ∩ ℕ ) = ( ℕ ∩ { 0 } )
7 0nnn ⊢ ¬ 0 ∈ ℕ
8 disjsn ⊢ ( ( ℕ ∩ { 0 } ) = ∅ ↔ ¬ 0 ∈ ℕ )
9 7 8 mpbir ⊢ ( ℕ ∩ { 0 } ) = ∅
10 6 9 eqtri ⊢ ( { 0 } ∩ ℕ ) = ∅
11 fimacnvdisj ⊢ ( ( ( 𝐼 × { 0 } ) : 𝐼 ⟶ { 0 } ∧ ( { 0 } ∩ ℕ ) = ∅ ) → ( ◡ ( 𝐼 × { 0 } ) “ ℕ ) = ∅ )
12 5 10 11 mp2an ⊢ ( ◡ ( 𝐼 × { 0 } ) “ ℕ ) = ∅
13 0fi ⊢ ∅ ∈ Fin
14 12 13 eqeltri ⊢ ( ◡ ( 𝐼 × { 0 } ) “ ℕ ) ∈ Fin
15 3 14 pm3.2i ⊢ ( ( 𝐼 × { 0 } ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝐼 × { 0 } ) “ ℕ ) ∈ Fin )
16 1 psrbag ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝐼 × { 0 } ) ∈ 𝐷 ↔ ( ( 𝐼 × { 0 } ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝐼 × { 0 } ) “ ℕ ) ∈ Fin ) ) )
17 15 16 mpbiri ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × { 0 } ) ∈ 𝐷 )