psrbaglefi

Description: There are finitely many bags dominated by a given bag. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Mario Carneiro, 25-Jan-2015) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024)

		Ref	Expression
	Hypothesis	psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	Assertion	psrbaglefi	$⊢ F \in D \to \{y \in D \| y \leq_{f} F\} \in Fin$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		df-rab	$⊢ \{y \in D \| y \leq_{f} F\} = \{y \| (y \in D \land y \leq_{f} F)\}$
3	1	psrbagf	$⊢ y \in D \to y : I ⟶ ℕ_{0}$
4	3	a1i	$⊢ F \in D \to (y \in D \to y : I ⟶ ℕ_{0})$
5	4	adantrd	$⊢ F \in D \to ((y \in D \land y \leq_{f} F) \to y : I ⟶ ℕ_{0})$
6		ss2ixp	$⊢ \forall x \in I (0 \dots F (x)) \subseteq ℕ_{0} \to \underset{x \in I}{⨉} (0 \dots F (x)) \subseteq \underset{x \in I}{⨉} ℕ_{0}$
7		fz0ssnn0	$⊢ (0 \dots F (x)) \subseteq ℕ_{0}$
8	7	a1i	$⊢ x \in I \to (0 \dots F (x)) \subseteq ℕ_{0}$
9	6 8	mprg	$⊢ \underset{x \in I}{⨉} (0 \dots F (x)) \subseteq \underset{x \in I}{⨉} ℕ_{0}$
10	9	sseli	$⊢ y \in \underset{x \in I}{⨉} (0 \dots F (x)) \to y \in \underset{x \in I}{⨉} ℕ_{0}$
11		vex	$⊢ y \in V$
12	11	elixpconst	$⊢ y \in \underset{x \in I}{⨉} ℕ_{0} \leftrightarrow y : I ⟶ ℕ_{0}$
13	10 12	sylib	$⊢ y \in \underset{x \in I}{⨉} (0 \dots F (x)) \to y : I ⟶ ℕ_{0}$
14	13	a1i	$⊢ F \in D \to (y \in \underset{x \in I}{⨉} (0 \dots F (x)) \to y : I ⟶ ℕ_{0})$
15		ffn	$⊢ y : I ⟶ ℕ_{0} \to y Fn I$
16	15	adantl	$⊢ (F \in D \land y : I ⟶ ℕ_{0}) \to y Fn I$
17	11	elixp	$⊢ y \in \underset{x \in I}{⨉} (0 \dots F (x)) \leftrightarrow (y Fn I \land \forall x \in I y (x) \in (0 \dots F (x)))$
18	17	baib	$⊢ y Fn I \to (y \in \underset{x \in I}{⨉} (0 \dots F (x)) \leftrightarrow \forall x \in I y (x) \in (0 \dots F (x)))$
19	16 18	syl	$⊢ (F \in D \land y : I ⟶ ℕ_{0}) \to (y \in \underset{x \in I}{⨉} (0 \dots F (x)) \leftrightarrow \forall x \in I y (x) \in (0 \dots F (x)))$
20		ffvelrn	$⊢ (y : I ⟶ ℕ_{0} \land x \in I) \to y (x) \in ℕ_{0}$
21	20	adantll	$⊢ ((F \in D \land y : I ⟶ ℕ_{0}) \land x \in I) \to y (x) \in ℕ_{0}$
22		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
23	21 22	eleqtrdi	$⊢ ((F \in D \land y : I ⟶ ℕ_{0}) \land x \in I) \to y (x) \in ℤ_{\geq 0}$
24	1	psrbagf	$⊢ F \in D \to F : I ⟶ ℕ_{0}$
25	24	adantr	$⊢ (F \in D \land y : I ⟶ ℕ_{0}) \to F : I ⟶ ℕ_{0}$
26	25	ffvelrnda	$⊢ ((F \in D \land y : I ⟶ ℕ_{0}) \land x \in I) \to F (x) \in ℕ_{0}$
27	26	nn0zd	$⊢ ((F \in D \land y : I ⟶ ℕ_{0}) \land x \in I) \to F (x) \in ℤ$
28		elfz5	$⊢ (y (x) \in ℤ_{\geq 0} \land F (x) \in ℤ) \to (y (x) \in (0 \dots F (x)) \leftrightarrow y (x) \leq F (x))$
29	23 27 28	syl2anc	$⊢ ((F \in D \land y : I ⟶ ℕ_{0}) \land x \in I) \to (y (x) \in (0 \dots F (x)) \leftrightarrow y (x) \leq F (x))$
30	29	ralbidva	$⊢ (F \in D \land y : I ⟶ ℕ_{0}) \to (\forall x \in I y (x) \in (0 \dots F (x)) \leftrightarrow \forall x \in I y (x) \leq F (x))$
31	24	ffnd	$⊢ F \in D \to F Fn I$
32	31	adantr	$⊢ (F \in D \land y : I ⟶ ℕ_{0}) \to F Fn I$
33	11	a1i	$⊢ (F \in D \land y : I ⟶ ℕ_{0}) \to y \in V$
34		simpl	$⊢ (F \in D \land y : I ⟶ ℕ_{0}) \to F \in D$
35		inidm	$⊢ I \cap I = I$
36		eqidd	$⊢ ((F \in D \land y : I ⟶ ℕ_{0}) \land x \in I) \to y (x) = y (x)$
37		eqidd	$⊢ ((F \in D \land y : I ⟶ ℕ_{0}) \land x \in I) \to F (x) = F (x)$
38	16 32 33 34 35 36 37	ofrfvalg	$⊢ (F \in D \land y : I ⟶ ℕ_{0}) \to (y \leq_{f} F \leftrightarrow \forall x \in I y (x) \leq F (x))$
39	30 38	bitr4d	$⊢ (F \in D \land y : I ⟶ ℕ_{0}) \to (\forall x \in I y (x) \in (0 \dots F (x)) \leftrightarrow y \leq_{f} F)$
40	1	psrbaglecl	$⊢ (F \in D \land y : I ⟶ ℕ_{0} \land y \leq_{f} F) \to y \in D$
41	40	3expia	$⊢ (F \in D \land y : I ⟶ ℕ_{0}) \to (y \leq_{f} F \to y \in D)$
42	41	pm4.71rd	$⊢ (F \in D \land y : I ⟶ ℕ_{0}) \to (y \leq_{f} F \leftrightarrow (y \in D \land y \leq_{f} F))$
43	19 39 42	3bitrrd	$⊢ (F \in D \land y : I ⟶ ℕ_{0}) \to ((y \in D \land y \leq_{f} F) \leftrightarrow y \in \underset{x \in I}{⨉} (0 \dots F (x)))$
44	43	ex	$⊢ F \in D \to (y : I ⟶ ℕ_{0} \to ((y \in D \land y \leq_{f} F) \leftrightarrow y \in \underset{x \in I}{⨉} (0 \dots F (x))))$
45	5 14 44	pm5.21ndd	$⊢ F \in D \to ((y \in D \land y \leq_{f} F) \leftrightarrow y \in \underset{x \in I}{⨉} (0 \dots F (x)))$
46	45	abbi1dv	$⊢ F \in D \to \{y \| (y \in D \land y \leq_{f} F)\} = \underset{x \in I}{⨉} (0 \dots F (x))$
47	2 46	syl5eq	$⊢ F \in D \to \{y \in D \| y \leq_{f} F\} = \underset{x \in I}{⨉} (0 \dots F (x))$
48		cnveq	$⊢ f = F \to f^{-1} = F^{-1}$
49	48	imaeq1d	$⊢ f = F \to f^{-1} [ℕ] = F^{-1} [ℕ]$
50	49	eleq1d	$⊢ f = F \to (f^{-1} [ℕ] \in Fin \leftrightarrow F^{-1} [ℕ] \in Fin)$
51	50 1	elrab2	$⊢ F \in D \leftrightarrow (F \in ({ℕ_{0}}^{I}) \land F^{-1} [ℕ] \in Fin)$
52	51	simprbi	$⊢ F \in D \to F^{-1} [ℕ] \in Fin$
53		fzfid	$⊢ (F \in D \land x \in I) \to (0 \dots F (x)) \in Fin$
54		frnnn0suppg	$⊢ (F \in D \land F : I ⟶ ℕ_{0}) \to F supp 0 = F^{-1} [ℕ]$
55	24 54	mpdan	$⊢ F \in D \to F supp 0 = F^{-1} [ℕ]$
56		eqimss	$⊢ F supp 0 = F^{-1} [ℕ] \to F supp 0 \subseteq F^{-1} [ℕ]$
57	55 56	syl	$⊢ F \in D \to F supp 0 \subseteq F^{-1} [ℕ]$
58		id	$⊢ F \in D \to F \in D$
59		c0ex	$⊢ 0 \in V$
60	59	a1i	$⊢ F \in D \to 0 \in V$
61	24 57 58 60	suppssrg	$⊢ (F \in D \land x \in (I ∖ F^{-1} [ℕ])) \to F (x) = 0$
62	61	oveq2d	$⊢ (F \in D \land x \in (I ∖ F^{-1} [ℕ])) \to (0 \dots F (x)) = (0 \dots 0)$
63		fz0sn	$⊢ (0 \dots 0) = \{0\}$
64	62 63	eqtrdi	$⊢ (F \in D \land x \in (I ∖ F^{-1} [ℕ])) \to (0 \dots F (x)) = \{0\}$
65		eqimss	$⊢ (0 \dots F (x)) = \{0\} \to (0 \dots F (x)) \subseteq \{0\}$
66	64 65	syl	$⊢ (F \in D \land x \in (I ∖ F^{-1} [ℕ])) \to (0 \dots F (x)) \subseteq \{0\}$
67	52 53 66	ixpfi2	$⊢ F \in D \to \underset{x \in I}{⨉} (0 \dots F (x)) \in Fin$
68	47 67	eqeltrd	$⊢ F \in D \to \{y \in D \| y \leq_{f} F\} \in Fin$

Metamath Proof Explorer

Theorem psrbaglefi

Proof