psrbaglefiOLD

Description: Obsolete version of psrbaglefi as of 6-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Mario Carneiro, 25-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Metamath Proof Explorer

Theorem psrbaglefiOLD

Proof