psrbagconf1o

Description: Bag complementation is a bijection on the set of bags dominated by a given bag F . (Contributed by Mario Carneiro, 29-Dec-2014) Remove a sethood antecedent. (Revised by SN, 6-Aug-2024)

	Ref	Expression
Hypotheses	psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	psrbagconf1o.s	$⊢ S = \{y \in D \| y \leq_{f} F\}$
Assertion	psrbagconf1o	$⊢ F \in D \to (x \in S ⟼ F -_{f} x) : S \underset{1-1 onto}{⟶} S$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		psrbagconf1o.s	$⊢ S = \{y \in D \| y \leq_{f} F\}$
3		eqid	$⊢ (x \in S ⟼ F -_{f} x) = (x \in S ⟼ F -_{f} x)$
4	1 2	psrbagconcl	$⊢ (F \in D \land x \in S) \to F -_{f} x \in S$
5	1 2	psrbagconcl	$⊢ (F \in D \land z \in S) \to F -_{f} z \in S$
6	1	psrbagf	$⊢ F \in D \to F : I ⟶ ℕ_{0}$
7	6	adantr	$⊢ (F \in D \land (x \in S \land z \in S)) \to F : I ⟶ ℕ_{0}$
8	7	ffvelrnda	$⊢ ((F \in D \land (x \in S \land z \in S)) \land n \in I) \to F (n) \in ℕ_{0}$
9	2	ssrab3	$⊢ S \subseteq D$
10	9	sseli	$⊢ z \in S \to z \in D$
11	10	adantl	$⊢ (F \in D \land z \in S) \to z \in D$
12	1	psrbagf	$⊢ z \in D \to z : I ⟶ ℕ_{0}$
13	11 12	syl	$⊢ (F \in D \land z \in S) \to z : I ⟶ ℕ_{0}$
14	13	adantrl	$⊢ (F \in D \land (x \in S \land z \in S)) \to z : I ⟶ ℕ_{0}$
15	14	ffvelrnda	$⊢ ((F \in D \land (x \in S \land z \in S)) \land n \in I) \to z (n) \in ℕ_{0}$
16		simprl	$⊢ (F \in D \land (x \in S \land z \in S)) \to x \in S$
17	9 16	sselid	$⊢ (F \in D \land (x \in S \land z \in S)) \to x \in D$
18	1	psrbagf	$⊢ x \in D \to x : I ⟶ ℕ_{0}$
19	17 18	syl	$⊢ (F \in D \land (x \in S \land z \in S)) \to x : I ⟶ ℕ_{0}$
20	19	ffvelrnda	$⊢ ((F \in D \land (x \in S \land z \in S)) \land n \in I) \to x (n) \in ℕ_{0}$
21		nn0cn	$⊢ F (n) \in ℕ_{0} \to F (n) \in ℂ$
22		nn0cn	$⊢ z (n) \in ℕ_{0} \to z (n) \in ℂ$
23		nn0cn	$⊢ x (n) \in ℕ_{0} \to x (n) \in ℂ$
24		subsub23	$⊢ (F (n) \in ℂ \land z (n) \in ℂ \land x (n) \in ℂ) \to (F (n) - z (n) = x (n) \leftrightarrow F (n) - x (n) = z (n))$
25	21 22 23 24	syl3an	$⊢ (F (n) \in ℕ_{0} \land z (n) \in ℕ_{0} \land x (n) \in ℕ_{0}) \to (F (n) - z (n) = x (n) \leftrightarrow F (n) - x (n) = z (n))$
26	8 15 20 25	syl3anc	$⊢ ((F \in D \land (x \in S \land z \in S)) \land n \in I) \to (F (n) - z (n) = x (n) \leftrightarrow F (n) - x (n) = z (n))$
27		eqcom	$⊢ x (n) = F (n) - z (n) \leftrightarrow F (n) - z (n) = x (n)$
28		eqcom	$⊢ z (n) = F (n) - x (n) \leftrightarrow F (n) - x (n) = z (n)$
29	26 27 28	3bitr4g	$⊢ ((F \in D \land (x \in S \land z \in S)) \land n \in I) \to (x (n) = F (n) - z (n) \leftrightarrow z (n) = F (n) - x (n))$
30	6	ffnd	$⊢ F \in D \to F Fn I$
31	30	adantr	$⊢ (F \in D \land (x \in S \land z \in S)) \to F Fn I$
32	13	ffnd	$⊢ (F \in D \land z \in S) \to z Fn I$
33	32	adantrl	$⊢ (F \in D \land (x \in S \land z \in S)) \to z Fn I$
34	19	ffnd	$⊢ (F \in D \land (x \in S \land z \in S)) \to x Fn I$
35	16 34	fndmexd	$⊢ (F \in D \land (x \in S \land z \in S)) \to I \in V$
36		inidm	$⊢ I \cap I = I$
37		eqidd	$⊢ ((F \in D \land (x \in S \land z \in S)) \land n \in I) \to F (n) = F (n)$
38		eqidd	$⊢ ((F \in D \land (x \in S \land z \in S)) \land n \in I) \to z (n) = z (n)$
39	31 33 35 35 36 37 38	ofval	$⊢ ((F \in D \land (x \in S \land z \in S)) \land n \in I) \to (F -_{f} z) (n) = F (n) - z (n)$
40	39	eqeq2d	$⊢ ((F \in D \land (x \in S \land z \in S)) \land n \in I) \to (x (n) = (F -_{f} z) (n) \leftrightarrow x (n) = F (n) - z (n))$
41		eqidd	$⊢ ((F \in D \land (x \in S \land z \in S)) \land n \in I) \to x (n) = x (n)$
42	31 34 35 35 36 37 41	ofval	$⊢ ((F \in D \land (x \in S \land z \in S)) \land n \in I) \to (F -_{f} x) (n) = F (n) - x (n)$
43	42	eqeq2d	$⊢ ((F \in D \land (x \in S \land z \in S)) \land n \in I) \to (z (n) = (F -_{f} x) (n) \leftrightarrow z (n) = F (n) - x (n))$
44	29 40 43	3bitr4d	$⊢ ((F \in D \land (x \in S \land z \in S)) \land n \in I) \to (x (n) = (F -_{f} z) (n) \leftrightarrow z (n) = (F -_{f} x) (n))$
45	44	ralbidva	$⊢ (F \in D \land (x \in S \land z \in S)) \to (\forall n \in I x (n) = (F -_{f} z) (n) \leftrightarrow \forall n \in I z (n) = (F -_{f} x) (n))$
46	5	adantrl	$⊢ (F \in D \land (x \in S \land z \in S)) \to F -_{f} z \in S$
47	9 46	sselid	$⊢ (F \in D \land (x \in S \land z \in S)) \to F -_{f} z \in D$
48	1	psrbagf	$⊢ F -_{f} z \in D \to (F -_{f} z) : I ⟶ ℕ_{0}$
49	47 48	syl	$⊢ (F \in D \land (x \in S \land z \in S)) \to (F -_{f} z) : I ⟶ ℕ_{0}$
50	49	ffnd	$⊢ (F \in D \land (x \in S \land z \in S)) \to (F -_{f} z) Fn I$
51		eqfnfv	$⊢ (x Fn I \land (F -_{f} z) Fn I) \to (x = F -_{f} z \leftrightarrow \forall n \in I x (n) = (F -_{f} z) (n))$
52	34 50 51	syl2anc	$⊢ (F \in D \land (x \in S \land z \in S)) \to (x = F -_{f} z \leftrightarrow \forall n \in I x (n) = (F -_{f} z) (n))$
53	9 4	sselid	$⊢ (F \in D \land x \in S) \to F -_{f} x \in D$
54	1	psrbagf	$⊢ F -_{f} x \in D \to (F -_{f} x) : I ⟶ ℕ_{0}$
55	53 54	syl	$⊢ (F \in D \land x \in S) \to (F -_{f} x) : I ⟶ ℕ_{0}$
56	55	ffnd	$⊢ (F \in D \land x \in S) \to (F -_{f} x) Fn I$
57	56	adantrr	$⊢ (F \in D \land (x \in S \land z \in S)) \to (F -_{f} x) Fn I$
58		eqfnfv	$⊢ (z Fn I \land (F -_{f} x) Fn I) \to (z = F -_{f} x \leftrightarrow \forall n \in I z (n) = (F -_{f} x) (n))$
59	33 57 58	syl2anc	$⊢ (F \in D \land (x \in S \land z \in S)) \to (z = F -_{f} x \leftrightarrow \forall n \in I z (n) = (F -_{f} x) (n))$
60	45 52 59	3bitr4d	$⊢ (F \in D \land (x \in S \land z \in S)) \to (x = F -_{f} z \leftrightarrow z = F -_{f} x)$
61	3 4 5 60	f1o2d	$⊢ F \in D \to (x \in S ⟼ F -_{f} x) : S \underset{1-1 onto}{⟶} S$

Metamath Proof Explorer

Theorem psrbagconf1o

Proof