actfunsnrndisj

Description: The action F of extending function from B to C with new values at point I yields different functions. (Contributed by Thierry Arnoux, 9-Dec-2021)

	Ref	Expression
Hypotheses	actfunsn.1	$⊢ (φ \land k \in C) \to A \subseteq C^{B}$
	actfunsn.2	$⊢ φ \to C \in V$
	actfunsn.3	$⊢ φ \to I \in V$
	actfunsn.4	$⊢ φ \to \neg I \in B$
	actfunsn.5	$⊢ F = (x \in A ⟼ x \cup \{⟨I, k⟩\})$
Assertion	actfunsnrndisj	$⊢ φ \to \underset{k \in C}{Disj} ran F$

Proof

Step	Hyp	Ref	Expression
1		actfunsn.1	$⊢ (φ \land k \in C) \to A \subseteq C^{B}$
2		actfunsn.2	$⊢ φ \to C \in V$
3		actfunsn.3	$⊢ φ \to I \in V$
4		actfunsn.4	$⊢ φ \to \neg I \in B$
5		actfunsn.5	$⊢ F = (x \in A ⟼ x \cup \{⟨I, k⟩\})$
6		simpr	$⊢ ((((φ \land k \in C) \land f \in ran F) \land z \in A) \land f = z \cup \{⟨I, k⟩\}) \to f = z \cup \{⟨I, k⟩\}$
7	6	fveq1d	$⊢ ((((φ \land k \in C) \land f \in ran F) \land z \in A) \land f = z \cup \{⟨I, k⟩\}) \to f (I) = (z \cup \{⟨I, k⟩\}) (I)$
8	1	ad2antrr	$⊢ (((φ \land k \in C) \land f \in ran F) \land z \in A) \to A \subseteq C^{B}$
9		simpr	$⊢ (((φ \land k \in C) \land f \in ran F) \land z \in A) \to z \in A$
10	8 9	sseldd	$⊢ (((φ \land k \in C) \land f \in ran F) \land z \in A) \to z \in (C^{B})$
11		elmapfn	$⊢ z \in (C^{B}) \to z Fn B$
12	10 11	syl	$⊢ (((φ \land k \in C) \land f \in ran F) \land z \in A) \to z Fn B$
13	3	ad3antrrr	$⊢ (((φ \land k \in C) \land f \in ran F) \land z \in A) \to I \in V$
14		simpllr	$⊢ (((φ \land k \in C) \land f \in ran F) \land z \in A) \to k \in C$
15		fnsng	$⊢ (I \in V \land k \in C) \to \{⟨I, k⟩\} Fn \{I\}$
16	13 14 15	syl2anc	$⊢ (((φ \land k \in C) \land f \in ran F) \land z \in A) \to \{⟨I, k⟩\} Fn \{I\}$
17		disjsn	$⊢ B \cap \{I\} = \emptyset \leftrightarrow \neg I \in B$
18	4 17	sylibr	$⊢ φ \to B \cap \{I\} = \emptyset$
19	18	ad3antrrr	$⊢ (((φ \land k \in C) \land f \in ran F) \land z \in A) \to B \cap \{I\} = \emptyset$
20		snidg	$⊢ I \in V \to I \in \{I\}$
21	13 20	syl	$⊢ (((φ \land k \in C) \land f \in ran F) \land z \in A) \to I \in \{I\}$
22		fvun2	$⊢ (z Fn B \land \{⟨I, k⟩\} Fn \{I\} \land (B \cap \{I\} = \emptyset \land I \in \{I\})) \to (z \cup \{⟨I, k⟩\}) (I) = \{⟨I, k⟩\} (I)$
23	12 16 19 21 22	syl112anc	$⊢ (((φ \land k \in C) \land f \in ran F) \land z \in A) \to (z \cup \{⟨I, k⟩\}) (I) = \{⟨I, k⟩\} (I)$
24		fvsng	$⊢ (I \in V \land k \in C) \to \{⟨I, k⟩\} (I) = k$
25	13 14 24	syl2anc	$⊢ (((φ \land k \in C) \land f \in ran F) \land z \in A) \to \{⟨I, k⟩\} (I) = k$
26	23 25	eqtrd	$⊢ (((φ \land k \in C) \land f \in ran F) \land z \in A) \to (z \cup \{⟨I, k⟩\}) (I) = k$
27	26	adantr	$⊢ ((((φ \land k \in C) \land f \in ran F) \land z \in A) \land f = z \cup \{⟨I, k⟩\}) \to (z \cup \{⟨I, k⟩\}) (I) = k$
28	7 27	eqtrd	$⊢ ((((φ \land k \in C) \land f \in ran F) \land z \in A) \land f = z \cup \{⟨I, k⟩\}) \to f (I) = k$
29		simpr	$⊢ ((φ \land k \in C) \land f \in ran F) \to f \in ran F$
30		uneq1	$⊢ x = z \to x \cup \{⟨I, k⟩\} = z \cup \{⟨I, k⟩\}$
31	30	cbvmptv	$⊢ (x \in A ⟼ x \cup \{⟨I, k⟩\}) = (z \in A ⟼ z \cup \{⟨I, k⟩\})$
32	5 31	eqtri	$⊢ F = (z \in A ⟼ z \cup \{⟨I, k⟩\})$
33		vex	$⊢ z \in V$
34		snex	$⊢ \{⟨I, k⟩\} \in V$
35	33 34	unex	$⊢ z \cup \{⟨I, k⟩\} \in V$
36	32 35	elrnmpti	$⊢ f \in ran F \leftrightarrow \exists z \in A f = z \cup \{⟨I, k⟩\}$
37	29 36	sylib	$⊢ ((φ \land k \in C) \land f \in ran F) \to \exists z \in A f = z \cup \{⟨I, k⟩\}$
38	28 37	r19.29a	$⊢ ((φ \land k \in C) \land f \in ran F) \to f (I) = k$
39	38	ralrimiva	$⊢ (φ \land k \in C) \to \forall f \in ran F f (I) = k$
40	39	ralrimiva	$⊢ φ \to \forall k \in C \forall f \in ran F f (I) = k$
41		invdisj	$⊢ \forall k \in C \forall f \in ran F f (I) = k \to \underset{k \in C}{Disj} ran F$
42	40 41	syl	$⊢ φ \to \underset{k \in C}{Disj} ran F$

Metamath Proof Explorer

Theorem actfunsnrndisj

Proof