actfunsnf1o

Description: The action F of extending function from B to C with new values at point I is a bijection. (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	actfunsnf1o	$⊢ (φ \land k \in C) \to F : A \underset{1-1 onto}{⟶} 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		uneq1	$⊢ x = z \to x \cup \{⟨I, k⟩\} = z \cup \{⟨I, k⟩\}$
7	6	cbvmptv	$⊢ (x \in A ⟼ x \cup \{⟨I, k⟩\}) = (z \in A ⟼ z \cup \{⟨I, k⟩\})$
8	5 7	eqtri	$⊢ F = (z \in A ⟼ z \cup \{⟨I, k⟩\})$
9		vex	$⊢ z \in V$
10		snex	$⊢ \{⟨I, k⟩\} \in V$
11	9 10	unex	$⊢ z \cup \{⟨I, k⟩\} \in V$
12	11	a1i	$⊢ ((φ \land k \in C) \land z \in A) \to z \cup \{⟨I, k⟩\} \in V$
13		vex	$⊢ y \in V$
14	13	resex	$⊢ {y ↾}_{B} \in V$
15	14	a1i	$⊢ ((φ \land k \in C) \land y \in ran F) \to {y ↾}_{B} \in V$
16		rspe	$⊢ (z \in A \land y = z \cup \{⟨I, k⟩\}) \to \exists z \in A y = z \cup \{⟨I, k⟩\}$
17	8 11	elrnmpti	$⊢ y \in ran F \leftrightarrow \exists z \in A y = z \cup \{⟨I, k⟩\}$
18	16 17	sylibr	$⊢ (z \in A \land y = z \cup \{⟨I, k⟩\}) \to y \in ran F$
19	18	adantll	$⊢ (((φ \land k \in C) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to y \in ran F$
20		simpr	$⊢ (((φ \land k \in C) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to y = z \cup \{⟨I, k⟩\}$
21	20	reseq1d	$⊢ (((φ \land k \in C) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to {y ↾}_{B} = {(z \cup \{⟨I, k⟩\}) ↾}_{B}$
22	1	sselda	$⊢ ((φ \land k \in C) \land z \in A) \to z \in (C^{B})$
23		elmapfn	$⊢ z \in (C^{B}) \to z Fn B$
24	22 23	syl	$⊢ ((φ \land k \in C) \land z \in A) \to z Fn B$
25		fnsng	$⊢ (I \in V \land k \in C) \to \{⟨I, k⟩\} Fn \{I\}$
26	3 25	sylan	$⊢ (φ \land k \in C) \to \{⟨I, k⟩\} Fn \{I\}$
27	26	adantr	$⊢ ((φ \land k \in C) \land z \in A) \to \{⟨I, k⟩\} Fn \{I\}$
28		disjsn	$⊢ B \cap \{I\} = \emptyset \leftrightarrow \neg I \in B$
29	4 28	sylibr	$⊢ φ \to B \cap \{I\} = \emptyset$
30	29	adantr	$⊢ (φ \land k \in C) \to B \cap \{I\} = \emptyset$
31	30	adantr	$⊢ ((φ \land k \in C) \land z \in A) \to B \cap \{I\} = \emptyset$
32		fnunres1	$⊢ (z Fn B \land \{⟨I, k⟩\} Fn \{I\} \land B \cap \{I\} = \emptyset) \to {(z \cup \{⟨I, k⟩\}) ↾}_{B} = z$
33	24 27 31 32	syl3anc	$⊢ ((φ \land k \in C) \land z \in A) \to {(z \cup \{⟨I, k⟩\}) ↾}_{B} = z$
34	33	adantr	$⊢ (((φ \land k \in C) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to {(z \cup \{⟨I, k⟩\}) ↾}_{B} = z$
35	21 34	eqtr2d	$⊢ (((φ \land k \in C) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to z = {y ↾}_{B}$
36	19 35	jca	$⊢ (((φ \land k \in C) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to (y \in ran F \land z = {y ↾}_{B})$
37	36	anasss	$⊢ ((φ \land k \in C) \land (z \in A \land y = z \cup \{⟨I, k⟩\})) \to (y \in ran F \land z = {y ↾}_{B})$
38		simpr	$⊢ (((φ \land k \in C) \land y \in ran F) \land z = {y ↾}_{B}) \to z = {y ↾}_{B}$
39		simpr	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to y = z \cup \{⟨I, k⟩\}$
40	39	reseq1d	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to {y ↾}_{B} = {(z \cup \{⟨I, k⟩\}) ↾}_{B}$
41	1	ad3antrrr	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to A \subseteq C^{B}$
42		simplr	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to z \in A$
43	41 42	sseldd	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to z \in (C^{B})$
44	43 23	syl	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to z Fn B$
45	3	ad4antr	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to I \in V$
46		simp-4r	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to k \in C$
47	45 46 25	syl2anc	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to \{⟨I, k⟩\} Fn \{I\}$
48	29	ad4antr	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to B \cap \{I\} = \emptyset$
49	44 47 48 32	syl3anc	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to {(z \cup \{⟨I, k⟩\}) ↾}_{B} = z$
50	49 42	eqeltrd	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to {(z \cup \{⟨I, k⟩\}) ↾}_{B} \in A$
51	40 50	eqeltrd	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to {y ↾}_{B} \in A$
52	17	bilani	$⊢ ((φ \land k \in C) \land y \in ran F) \to \exists z \in A y = z \cup \{⟨I, k⟩\}$
53	51 52	r19.29a	$⊢ ((φ \land k \in C) \land y \in ran F) \to {y ↾}_{B} \in A$
54	53	adantr	$⊢ (((φ \land k \in C) \land y \in ran F) \land z = {y ↾}_{B}) \to {y ↾}_{B} \in A$
55	38 54	eqeltrd	$⊢ (((φ \land k \in C) \land y \in ran F) \land z = {y ↾}_{B}) \to z \in A$
56	38	uneq1d	$⊢ (((φ \land k \in C) \land y \in ran F) \land z = {y ↾}_{B}) \to z \cup \{⟨I, k⟩\} = ({y ↾}_{B}) \cup \{⟨I, k⟩\}$
57	40 49	eqtrd	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to {y ↾}_{B} = z$
58	57	uneq1d	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to ({y ↾}_{B}) \cup \{⟨I, k⟩\} = z \cup \{⟨I, k⟩\}$
59	58 39	eqtr4d	$⊢ ((((φ \land k \in C) \land y \in ran F) \land z \in A) \land y = z \cup \{⟨I, k⟩\}) \to ({y ↾}_{B}) \cup \{⟨I, k⟩\} = y$
60	59 52	r19.29a	$⊢ ((φ \land k \in C) \land y \in ran F) \to ({y ↾}_{B}) \cup \{⟨I, k⟩\} = y$
61	60	adantr	$⊢ (((φ \land k \in C) \land y \in ran F) \land z = {y ↾}_{B}) \to ({y ↾}_{B}) \cup \{⟨I, k⟩\} = y$
62	56 61	eqtr2d	$⊢ (((φ \land k \in C) \land y \in ran F) \land z = {y ↾}_{B}) \to y = z \cup \{⟨I, k⟩\}$
63	55 62	jca	$⊢ (((φ \land k \in C) \land y \in ran F) \land z = {y ↾}_{B}) \to (z \in A \land y = z \cup \{⟨I, k⟩\})$
64	63	anasss	$⊢ ((φ \land k \in C) \land (y \in ran F \land z = {y ↾}_{B})) \to (z \in A \land y = z \cup \{⟨I, k⟩\})$
65	37 64	impbida	$⊢ (φ \land k \in C) \to ((z \in A \land y = z \cup \{⟨I, k⟩\}) \leftrightarrow (y \in ran F \land z = {y ↾}_{B}))$
66	8 12 15 65	f1od	$⊢ (φ \land k \in C) \to F : A \underset{1-1 onto}{⟶} ran F$

Metamath Proof Explorer

Theorem actfunsnf1o

Proof