fnsuppres

Description: Two ways to express restriction of a support set. (Contributed by Stefan O'Rear, 5-Feb-2015) (Revised by AV, 28-May-2019)

		Ref	Expression
	Assertion	fnsuppres	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to (F supp Z \subseteq A \leftrightarrow {F ↾}_{B} = B \times \{Z\})$

Proof

Step	Hyp	Ref	Expression
1		fndm	$⊢ F Fn (A \cup B) \to dom F = A \cup B$
2	1	rabeqdv	$⊢ F Fn (A \cup B) \to \{a \in dom F \| F (a) \neq Z\} = \{a \in (A \cup B) \| F (a) \neq Z\}$
3	2	3ad2ant1	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to \{a \in dom F \| F (a) \neq Z\} = \{a \in (A \cup B) \| F (a) \neq Z\}$
4	3	sseq1d	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to (\{a \in dom F \| F (a) \neq Z\} \subseteq A \leftrightarrow \{a \in (A \cup B) \| F (a) \neq Z\} \subseteq A)$
5		unss	$⊢ (\{a \in A \| F (a) \neq Z\} \subseteq A \land \{a \in B \| F (a) \neq Z\} \subseteq A) \leftrightarrow \{a \in A \| F (a) \neq Z\} \cup \{a \in B \| F (a) \neq Z\} \subseteq A$
6		ssrab2	$⊢ \{a \in A \| F (a) \neq Z\} \subseteq A$
7	6	biantrur	$⊢ \{a \in B \| F (a) \neq Z\} \subseteq A \leftrightarrow (\{a \in A \| F (a) \neq Z\} \subseteq A \land \{a \in B \| F (a) \neq Z\} \subseteq A)$
8		rabun2	$⊢ \{a \in (A \cup B) \| F (a) \neq Z\} = \{a \in A \| F (a) \neq Z\} \cup \{a \in B \| F (a) \neq Z\}$
9	8	sseq1i	$⊢ \{a \in (A \cup B) \| F (a) \neq Z\} \subseteq A \leftrightarrow \{a \in A \| F (a) \neq Z\} \cup \{a \in B \| F (a) \neq Z\} \subseteq A$
10	5 7 9	3bitr4ri	$⊢ \{a \in (A \cup B) \| F (a) \neq Z\} \subseteq A \leftrightarrow \{a \in B \| F (a) \neq Z\} \subseteq A$
11		rabss	$⊢ \{a \in B \| F (a) \neq Z\} \subseteq A \leftrightarrow \forall a \in B (F (a) \neq Z \to a \in A)$
12		fvres	$⊢ a \in B \to ({F ↾}_{B}) (a) = F (a)$
13	12	adantl	$⊢ ((F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \land a \in B) \to ({F ↾}_{B}) (a) = F (a)$
14		simp2r	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to Z \in V$
15		fvconst2g	$⊢ (Z \in V \land a \in B) \to (B \times \{Z\}) (a) = Z$
16	14 15	sylan	$⊢ ((F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \land a \in B) \to (B \times \{Z\}) (a) = Z$
17	13 16	eqeq12d	$⊢ ((F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \land a \in B) \to (({F ↾}_{B}) (a) = (B \times \{Z\}) (a) \leftrightarrow F (a) = Z)$
18		nne	$⊢ \neg F (a) \neq Z \leftrightarrow F (a) = Z$
19	18	a1i	$⊢ ((F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \land a \in B) \to (\neg F (a) \neq Z \leftrightarrow F (a) = Z)$
20		id	$⊢ a \in B \to a \in B$
21		simp3	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to A \cap B = \emptyset$
22		minel	$⊢ (a \in B \land A \cap B = \emptyset) \to \neg a \in A$
23	20 21 22	syl2anr	$⊢ ((F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \land a \in B) \to \neg a \in A$
24		mtt	$⊢ \neg a \in A \to (\neg F (a) \neq Z \leftrightarrow (F (a) \neq Z \to a \in A))$
25	23 24	syl	$⊢ ((F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \land a \in B) \to (\neg F (a) \neq Z \leftrightarrow (F (a) \neq Z \to a \in A))$
26	17 19 25	3bitr2rd	$⊢ ((F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \land a \in B) \to ((F (a) \neq Z \to a \in A) \leftrightarrow ({F ↾}_{B}) (a) = (B \times \{Z\}) (a))$
27	26	ralbidva	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to (\forall a \in B (F (a) \neq Z \to a \in A) \leftrightarrow \forall a \in B ({F ↾}_{B}) (a) = (B \times \{Z\}) (a))$
28	11 27	bitrid	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to (\{a \in B \| F (a) \neq Z\} \subseteq A \leftrightarrow \forall a \in B ({F ↾}_{B}) (a) = (B \times \{Z\}) (a))$
29	10 28	bitrid	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to (\{a \in (A \cup B) \| F (a) \neq Z\} \subseteq A \leftrightarrow \forall a \in B ({F ↾}_{B}) (a) = (B \times \{Z\}) (a))$
30	4 29	bitrd	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to (\{a \in dom F \| F (a) \neq Z\} \subseteq A \leftrightarrow \forall a \in B ({F ↾}_{B}) (a) = (B \times \{Z\}) (a))$
31		fnfun	$⊢ F Fn (A \cup B) \to Fun F$
32	31	3anim1i	$⊢ (F Fn (A \cup B) \land F \in W \land Z \in V) \to (Fun F \land F \in W \land Z \in V)$
33	32	3expb	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V)) \to (Fun F \land F \in W \land Z \in V)$
34		suppval1	$⊢ (Fun F \land F \in W \land Z \in V) \to F supp Z = \{a \in dom F \| F (a) \neq Z\}$
35	33 34	syl	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V)) \to F supp Z = \{a \in dom F \| F (a) \neq Z\}$
36	35	3adant3	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to F supp Z = \{a \in dom F \| F (a) \neq Z\}$
37	36	sseq1d	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to (F supp Z \subseteq A \leftrightarrow \{a \in dom F \| F (a) \neq Z\} \subseteq A)$
38		simp1	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to F Fn (A \cup B)$
39		ssun2	$⊢ B \subseteq A \cup B$
40	39	a1i	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to B \subseteq A \cup B$
41		fnssres	$⊢ (F Fn (A \cup B) \land B \subseteq A \cup B) \to ({F ↾}_{B}) Fn B$
42	38 40 41	syl2anc	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to ({F ↾}_{B}) Fn B$
43		fnconstg	$⊢ Z \in V \to (B \times \{Z\}) Fn B$
44	43	adantl	$⊢ (F \in W \land Z \in V) \to (B \times \{Z\}) Fn B$
45	44	3ad2ant2	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to (B \times \{Z\}) Fn B$
46		eqfnfv	$⊢ (({F ↾}_{B}) Fn B \land (B \times \{Z\}) Fn B) \to ({F ↾}_{B} = B \times \{Z\} \leftrightarrow \forall a \in B ({F ↾}_{B}) (a) = (B \times \{Z\}) (a))$
47	42 45 46	syl2anc	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to ({F ↾}_{B} = B \times \{Z\} \leftrightarrow \forall a \in B ({F ↾}_{B}) (a) = (B \times \{Z\}) (a))$
48	30 37 47	3bitr4d	$⊢ (F Fn (A \cup B) \land (F \in W \land Z \in V) \land A \cap B = \emptyset) \to (F supp Z \subseteq A \leftrightarrow {F ↾}_{B} = B \times \{Z\})$

Metamath Proof Explorer

Theorem fnsuppres

Proof