psrbag0

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

		Ref	Expression
	Hypothesis	psrbag0.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	Assertion	psrbag0	$⊢ I \in V \to I \times \{0\} \in D$

Step	Hyp	Ref	Expression
1		psrbag0.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		0nn0	$⊢ 0 \in ℕ_{0}$
3	2	fconst6	$⊢ (I \times \{0\}) : I ⟶ ℕ_{0}$
4		c0ex	$⊢ 0 \in V$
5	4	fconst	$⊢ (I \times \{0\}) : I ⟶ \{0\}$
6		incom	$⊢ \{0\} \cap ℕ = ℕ \cap \{0\}$
7		0nnn	$⊢ \neg 0 \in ℕ$
8		disjsn	$⊢ ℕ \cap \{0\} = \emptyset \leftrightarrow \neg 0 \in ℕ$
9	7 8	mpbir	$⊢ ℕ \cap \{0\} = \emptyset$
10	6 9	eqtri	$⊢ \{0\} \cap ℕ = \emptyset$
11		fimacnvdisj	$⊢ ((I \times \{0\}) : I ⟶ \{0\} \land \{0\} \cap ℕ = \emptyset) \to {(I \times \{0\})}^{-1} [ℕ] = \emptyset$
12	5 10 11	mp2an	$⊢ {(I \times \{0\})}^{-1} [ℕ] = \emptyset$
13		0fi	$⊢ \emptyset \in Fin$
14	12 13	eqeltri	$⊢ {(I \times \{0\})}^{-1} [ℕ] \in Fin$
15	3 14	pm3.2i	$⊢ ((I \times \{0\}) : I ⟶ ℕ_{0} \land {(I \times \{0\})}^{-1} [ℕ] \in Fin)$
16	1	psrbag	$⊢ I \in V \to (I \times \{0\} \in D \leftrightarrow ((I \times \{0\}) : I ⟶ ℕ_{0} \land {(I \times \{0\})}^{-1} [ℕ] \in Fin))$
17	15 16	mpbiri	$⊢ I \in V \to I \times \{0\} \in D$

Metamath Proof Explorer