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		0fin	⊢ ∅ ∈ 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 } ) ∈ 𝐷 )