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)

	Ref	Expression
Hypotheses	psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	psrbagconf1o.1	$⊢ S = \{y \in D \| y \leq_{f} F\}$
Assertion	psrbagconf1o	$⊢ (I \in V \land 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.1	$⊢ S = \{y \in D \| y \leq_{f} F\}$
3		eqid	$⊢ (x \in S ⟼ F -_{f} x) = (x \in S ⟼ F -_{f} x)$
4		simpll	$⊢ ((I \in V \land F \in D) \land x \in S) \to I \in V$
5		simplr	$⊢ ((I \in V \land F \in D) \land x \in S) \to F \in D$
6		simpr	$⊢ ((I \in V \land F \in D) \land x \in S) \to x \in S$
7		breq1	$⊢ y = x \to (y \leq_{f} F \leftrightarrow x \leq_{f} F)$
8	7 2	elrab2	$⊢ x \in S \leftrightarrow (x \in D \land x \leq_{f} F)$
9	6 8	sylib	$⊢ ((I \in V \land F \in D) \land x \in S) \to (x \in D \land x \leq_{f} F)$
10	9	simpld	$⊢ ((I \in V \land F \in D) \land x \in S) \to x \in D$
11	1	psrbagf	$⊢ (I \in V \land x \in D) \to x : I ⟶ ℕ_{0}$
12	4 10 11	syl2anc	$⊢ ((I \in V \land F \in D) \land x \in S) \to x : I ⟶ ℕ_{0}$
13	9	simprd	$⊢ ((I \in V \land F \in D) \land x \in S) \to x \leq_{f} F$
14	1	psrbagcon	$⊢ (I \in V \land (F \in D \land x : I ⟶ ℕ_{0} \land x \leq_{f} F)) \to (F -_{f} x \in D \land (F -_{f} x) \leq_{f} F)$
15	4 5 12 13 14	syl13anc	$⊢ ((I \in V \land F \in D) \land x \in S) \to (F -_{f} x \in D \land (F -_{f} x) \leq_{f} F)$
16		breq1	$⊢ y = F -_{f} x \to (y \leq_{f} F \leftrightarrow (F -_{f} x) \leq_{f} F)$
17	16 2	elrab2	$⊢ F -_{f} x \in S \leftrightarrow (F -_{f} x \in D \land (F -_{f} x) \leq_{f} F)$
18	15 17	sylibr	$⊢ ((I \in V \land F \in D) \land x \in S) \to F -_{f} x \in S$
19	18	ralrimiva	$⊢ (I \in V \land F \in D) \to \forall x \in S F -_{f} x \in S$
20		oveq2	$⊢ x = z \to F -_{f} x = F -_{f} z$
21	20	eleq1d	$⊢ x = z \to (F -_{f} x \in S \leftrightarrow F -_{f} z \in S)$
22	21	rspccva	$⊢ (\forall x \in S F -_{f} x \in S \land z \in S) \to F -_{f} z \in S$
23	19 22	sylan	$⊢ ((I \in V \land F \in D) \land z \in S) \to F -_{f} z \in S$
24	1	psrbagf	$⊢ (I \in V \land F \in D) \to F : I ⟶ ℕ_{0}$
25	24	adantr	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to F : I ⟶ ℕ_{0}$
26	25	ffvelrnda	$⊢ (((I \in V \land F \in D) \land (x \in S \land z \in S)) \land n \in I) \to F (n) \in ℕ_{0}$
27		simpll	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to I \in V$
28	2	ssrab3	$⊢ S \subseteq D$
29		simprr	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to z \in S$
30	28 29	sseldi	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to z \in D$
31	1	psrbagf	$⊢ (I \in V \land z \in D) \to z : I ⟶ ℕ_{0}$
32	27 30 31	syl2anc	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to z : I ⟶ ℕ_{0}$
33	32	ffvelrnda	$⊢ (((I \in V \land F \in D) \land (x \in S \land z \in S)) \land n \in I) \to z (n) \in ℕ_{0}$
34	12	adantrr	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to x : I ⟶ ℕ_{0}$
35	34	ffvelrnda	$⊢ (((I \in V \land F \in D) \land (x \in S \land z \in S)) \land n \in I) \to x (n) \in ℕ_{0}$
36		nn0cn	$⊢ F (n) \in ℕ_{0} \to F (n) \in ℂ$
37		nn0cn	$⊢ z (n) \in ℕ_{0} \to z (n) \in ℂ$
38		nn0cn	$⊢ x (n) \in ℕ_{0} \to x (n) \in ℂ$
39		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))$
40	36 37 38 39	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))$
41	26 33 35 40	syl3anc	$⊢ (((I \in V \land 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))$
42		eqcom	$⊢ x (n) = F (n) - z (n) \leftrightarrow F (n) - z (n) = x (n)$
43		eqcom	$⊢ z (n) = F (n) - x (n) \leftrightarrow F (n) - x (n) = z (n)$
44	41 42 43	3bitr4g	$⊢ (((I \in V \land 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))$
45	25	ffnd	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to F Fn I$
46	32	ffnd	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to z Fn I$
47		inidm	$⊢ I \cap I = I$
48		eqidd	$⊢ (((I \in V \land F \in D) \land (x \in S \land z \in S)) \land n \in I) \to F (n) = F (n)$
49		eqidd	$⊢ (((I \in V \land F \in D) \land (x \in S \land z \in S)) \land n \in I) \to z (n) = z (n)$
50	45 46 27 27 47 48 49	ofval	$⊢ (((I \in V \land F \in D) \land (x \in S \land z \in S)) \land n \in I) \to (F -_{f} z) (n) = F (n) - z (n)$
51	50	eqeq2d	$⊢ (((I \in V \land 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))$
52	34	ffnd	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to x Fn I$
53		eqidd	$⊢ (((I \in V \land F \in D) \land (x \in S \land z \in S)) \land n \in I) \to x (n) = x (n)$
54	45 52 27 27 47 48 53	ofval	$⊢ (((I \in V \land F \in D) \land (x \in S \land z \in S)) \land n \in I) \to (F -_{f} x) (n) = F (n) - x (n)$
55	54	eqeq2d	$⊢ (((I \in V \land 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))$
56	44 51 55	3bitr4d	$⊢ (((I \in V \land 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))$
57	56	ralbidva	$⊢ ((I \in V \land 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))$
58	23	adantrl	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to F -_{f} z \in S$
59	28 58	sseldi	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to F -_{f} z \in D$
60	1	psrbagf	$⊢ (I \in V \land F -_{f} z \in D) \to (F -_{f} z) : I ⟶ ℕ_{0}$
61	27 59 60	syl2anc	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to (F -_{f} z) : I ⟶ ℕ_{0}$
62	61	ffnd	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to (F -_{f} z) Fn I$
63		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))$
64	52 62 63	syl2anc	$⊢ ((I \in V \land 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))$
65	18	adantrr	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to F -_{f} x \in S$
66	28 65	sseldi	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to F -_{f} x \in D$
67	1	psrbagf	$⊢ (I \in V \land F -_{f} x \in D) \to (F -_{f} x) : I ⟶ ℕ_{0}$
68	27 66 67	syl2anc	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to (F -_{f} x) : I ⟶ ℕ_{0}$
69	68	ffnd	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to (F -_{f} x) Fn I$
70		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))$
71	46 69 70	syl2anc	$⊢ ((I \in V \land 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))$
72	57 64 71	3bitr4d	$⊢ ((I \in V \land F \in D) \land (x \in S \land z \in S)) \to (x = F -_{f} z \leftrightarrow z = F -_{f} x)$
73	3 18 23 72	f1o2d	$⊢ (I \in V \land F \in D) \to (x \in S ⟼ F -_{f} x) : S \underset{1-1 onto}{⟶} S$

Metamath Proof Explorer

Theorem psrbagconf1o

Proof