2ndresdju

Description: The 2nd function restricted to a disjoint union is injective. (Contributed by Thierry Arnoux, 23-Jun-2024)

	Ref	Expression
Hypotheses	2ndresdju.u	$⊢ U = ⋃_{x \in X} (\{x\} \times C)$
	2ndresdju.a	$⊢ φ \to A \in V$
	2ndresdju.x	$⊢ φ \to X \in W$
	2ndresdju.1	$⊢ φ \to \underset{x \in X}{Disj} C$
	2ndresdju.2	$⊢ φ \to ⋃_{x \in X} C = A$
Assertion	2ndresdju	$⊢ φ \to ({2^{nd} ↾}_{U}) : U \underset{1-1}{⟶} A$

Proof

Step	Hyp	Ref	Expression
1		2ndresdju.u	$⊢ U = ⋃_{x \in X} (\{x\} \times C)$
2		2ndresdju.a	$⊢ φ \to A \in V$
3		2ndresdju.x	$⊢ φ \to X \in W$
4		2ndresdju.1	$⊢ φ \to \underset{x \in X}{Disj} C$
5		2ndresdju.2	$⊢ φ \to ⋃_{x \in X} C = A$
6		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
7		fofn	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} Fn V$
8	6 7	mp1i	$⊢ φ \to 2^{nd} Fn V$
9		ssv	$⊢ U \subseteq V$
10	9	a1i	$⊢ φ \to U \subseteq V$
11	8 10	fnssresd	$⊢ φ \to ({2^{nd} ↾}_{U}) Fn U$
12		simpr	$⊢ (φ \land u \in U) \to u \in U$
13	12	fvresd	$⊢ (φ \land u \in U) \to ({2^{nd} ↾}_{U}) (u) = 2^{nd} (u)$
14		djussxp2	$⊢ ⋃_{x \in X} (\{x\} \times C) \subseteq X \times ⋃_{x \in X} C$
15	5	xpeq2d	$⊢ φ \to X \times ⋃_{x \in X} C = X \times A$
16	14 15	sseqtrid	$⊢ φ \to ⋃_{x \in X} (\{x\} \times C) \subseteq X \times A$
17	1 16	eqsstrid	$⊢ φ \to U \subseteq X \times A$
18	17	sselda	$⊢ (φ \land u \in U) \to u \in (X \times A)$
19		xp2nd	$⊢ u \in (X \times A) \to 2^{nd} (u) \in A$
20	18 19	syl	$⊢ (φ \land u \in U) \to 2^{nd} (u) \in A$
21	13 20	eqeltrd	$⊢ (φ \land u \in U) \to ({2^{nd} ↾}_{U}) (u) \in A$
22	21	ralrimiva	$⊢ φ \to \forall u \in U ({2^{nd} ↾}_{U}) (u) \in A$
23		ffnfv	$⊢ ({2^{nd} ↾}_{U}) : U ⟶ A \leftrightarrow (({2^{nd} ↾}_{U}) Fn U \land \forall u \in U ({2^{nd} ↾}_{U}) (u) \in A)$
24	11 22 23	sylanbrc	$⊢ φ \to ({2^{nd} ↾}_{U}) : U ⟶ A$
25		nfv	$⊢ Ⅎ x φ$
26		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in X} (\{x\} \times C)$
27	1 26	nfcxfr	$⊢ \underline{Ⅎ} x U$
28	27	nfcri	$⊢ Ⅎ x u \in U$
29	25 28	nfan	$⊢ Ⅎ x (φ \land u \in U)$
30	27	nfcri	$⊢ Ⅎ x v \in U$
31	29 30	nfan	$⊢ Ⅎ x ((φ \land u \in U) \land v \in U)$
32		nfcv	$⊢ \underline{Ⅎ} x 2^{nd}$
33	32 27	nfres	$⊢ \underline{Ⅎ} x ({2^{nd} ↾}_{U})$
34		nfcv	$⊢ \underline{Ⅎ} x u$
35	33 34	nffv	$⊢ \underline{Ⅎ} x ({2^{nd} ↾}_{U}) (u)$
36		nfcv	$⊢ \underline{Ⅎ} x v$
37	33 36	nffv	$⊢ \underline{Ⅎ} x ({2^{nd} ↾}_{U}) (v)$
38	35 37	nfeq	$⊢ Ⅎ x ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)$
39	31 38	nfan	$⊢ Ⅎ x (((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v))$
40		nfv	$⊢ Ⅎ x u = v$
41	1	eleq2i	$⊢ u \in U \leftrightarrow u \in ⋃_{x \in X} (\{x\} \times C)$
42		eliunxp	$⊢ u \in ⋃_{x \in X} (\{x\} \times C) \leftrightarrow \exists x \exists c (u = ⟨x, c⟩ \land (x \in X \land c \in C))$
43	41 42	sylbb	$⊢ u \in U \to \exists x \exists c (u = ⟨x, c⟩ \land (x \in X \land c \in C))$
44	43	ad3antlr	$⊢ (((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \to \exists x \exists c (u = ⟨x, c⟩ \land (x \in X \land c \in C))$
45	1	eleq2i	$⊢ v \in U \leftrightarrow v \in ⋃_{x \in X} (\{x\} \times C)$
46		eliunxp	$⊢ v \in ⋃_{x \in X} (\{x\} \times C) \leftrightarrow \exists x \exists d (v = ⟨x, d⟩ \land (x \in X \land d \in C))$
47	45 46	bitri	$⊢ v \in U \leftrightarrow \exists x \exists d (v = ⟨x, d⟩ \land (x \in X \land d \in C))$
48		nfv	$⊢ Ⅎ y \exists d (v = ⟨x, d⟩ \land (x \in X \land d \in C))$
49		nfv	$⊢ Ⅎ x v = ⟨y, d⟩$
50		nfv	$⊢ Ⅎ x y \in X$
51		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ C$
52	51	nfcri	$⊢ Ⅎ x d \in ⦋ y / x ⦌ C$
53	50 52	nfan	$⊢ Ⅎ x (y \in X \land d \in ⦋ y / x ⦌ C)$
54	49 53	nfan	$⊢ Ⅎ x (v = ⟨y, d⟩ \land (y \in X \land d \in ⦋ y / x ⦌ C))$
55	54	nfex	$⊢ Ⅎ x \exists d (v = ⟨y, d⟩ \land (y \in X \land d \in ⦋ y / x ⦌ C))$
56		opeq1	$⊢ x = y \to ⟨x, d⟩ = ⟨y, d⟩$
57	56	eqeq2d	$⊢ x = y \to (v = ⟨x, d⟩ \leftrightarrow v = ⟨y, d⟩)$
58		eleq1w	$⊢ x = y \to (x \in X \leftrightarrow y \in X)$
59		csbeq1a	$⊢ x = y \to C = ⦋ y / x ⦌ C$
60	59	eleq2d	$⊢ x = y \to (d \in C \leftrightarrow d \in ⦋ y / x ⦌ C)$
61	58 60	anbi12d	$⊢ x = y \to ((x \in X \land d \in C) \leftrightarrow (y \in X \land d \in ⦋ y / x ⦌ C))$
62	57 61	anbi12d	$⊢ x = y \to ((v = ⟨x, d⟩ \land (x \in X \land d \in C)) \leftrightarrow (v = ⟨y, d⟩ \land (y \in X \land d \in ⦋ y / x ⦌ C)))$
63	62	exbidv	$⊢ x = y \to (\exists d (v = ⟨x, d⟩ \land (x \in X \land d \in C)) \leftrightarrow \exists d (v = ⟨y, d⟩ \land (y \in X \land d \in ⦋ y / x ⦌ C)))$
64	48 55 63	cbvexv1	$⊢ \exists x \exists d (v = ⟨x, d⟩ \land (x \in X \land d \in C)) \leftrightarrow \exists y \exists d (v = ⟨y, d⟩ \land (y \in X \land d \in ⦋ y / x ⦌ C))$
65	47 64	sylbb	$⊢ v \in U \to \exists y \exists d (v = ⟨y, d⟩ \land (y \in X \land d \in ⦋ y / x ⦌ C))$
66	65	ad5antlr	$⊢ ((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \to \exists y \exists d (v = ⟨y, d⟩ \land (y \in X \land d \in ⦋ y / x ⦌ C))$
67	4	ad9antr	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to \underset{x \in X}{Disj} C$
68		simp-5r	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to x \in X$
69		simplr	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to y \in X$
70		simp-4r	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to c \in C$
71		simp-7r	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)$
72		simp-9r	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to u \in U$
73	72	fvresd	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to ({2^{nd} ↾}_{U}) (u) = 2^{nd} (u)$
74		simp-6r	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to u = ⟨x, c⟩$
75	74	fveq2d	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to 2^{nd} (u) = 2^{nd} (⟨x, c⟩)$
76		vex	$⊢ x \in V$
77		vex	$⊢ c \in V$
78	76 77	op2nd	$⊢ 2^{nd} (⟨x, c⟩) = c$
79	75 78	eqtrdi	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to 2^{nd} (u) = c$
80	73 79	eqtrd	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to ({2^{nd} ↾}_{U}) (u) = c$
81		simp-8r	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to v \in U$
82	81	fvresd	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to ({2^{nd} ↾}_{U}) (v) = 2^{nd} (v)$
83		simpllr	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to v = ⟨y, d⟩$
84	83	fveq2d	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to 2^{nd} (v) = 2^{nd} (⟨y, d⟩)$
85		vex	$⊢ y \in V$
86		vex	$⊢ d \in V$
87	85 86	op2nd	$⊢ 2^{nd} (⟨y, d⟩) = d$
88	84 87	eqtrdi	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to 2^{nd} (v) = d$
89	82 88	eqtrd	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to ({2^{nd} ↾}_{U}) (v) = d$
90	71 80 89	3eqtr3d	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to c = d$
91		simpr	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to d \in ⦋ y / x ⦌ C$
92	90 91	eqeltrd	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to c \in ⦋ y / x ⦌ C$
93	51 59	disjif	$⊢ (\underset{x \in X}{Disj} C \land (x \in X \land y \in X) \land (c \in C \land c \in ⦋ y / x ⦌ C)) \to x = y$
94	67 68 69 70 92 93	syl122anc	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to x = y$
95	94 90	opeq12d	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to ⟨x, c⟩ = ⟨y, d⟩$
96	95 74 83	3eqtr4d	$⊢ (((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land y \in X) \land d \in ⦋ y / x ⦌ C) \to u = v$
97	96	anasss	$⊢ ((((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \land v = ⟨y, d⟩) \land (y \in X \land d \in ⦋ y / x ⦌ C)) \to u = v$
98	97	expl	$⊢ ((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \to ((v = ⟨y, d⟩ \land (y \in X \land d \in ⦋ y / x ⦌ C)) \to u = v)$
99	98	exlimdvv	$⊢ ((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \to (\exists y \exists d (v = ⟨y, d⟩ \land (y \in X \land d \in ⦋ y / x ⦌ C)) \to u = v)$
100	66 99	mpd	$⊢ ((((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land x \in X) \land c \in C) \to u = v$
101	100	anasss	$⊢ (((((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \land u = ⟨x, c⟩) \land (x \in X \land c \in C)) \to u = v$
102	101	expl	$⊢ (((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \to ((u = ⟨x, c⟩ \land (x \in X \land c \in C)) \to u = v)$
103	102	exlimdv	$⊢ (((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \to (\exists c (u = ⟨x, c⟩ \land (x \in X \land c \in C)) \to u = v)$
104	39 40 44 103	exlimimdd	$⊢ (((φ \land u \in U) \land v \in U) \land ({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v)) \to u = v$
105	104	ex	$⊢ ((φ \land u \in U) \land v \in U) \to (({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v) \to u = v)$
106	105	anasss	$⊢ (φ \land (u \in U \land v \in U)) \to (({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v) \to u = v)$
107	106	ralrimivva	$⊢ φ \to \forall u \in U \forall v \in U (({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v) \to u = v)$
108		dff13	$⊢ ({2^{nd} ↾}_{U}) : U \underset{1-1}{⟶} A \leftrightarrow (({2^{nd} ↾}_{U}) : U ⟶ A \land \forall u \in U \forall v \in U (({2^{nd} ↾}_{U}) (u) = ({2^{nd} ↾}_{U}) (v) \to u = v))$
109	24 107 108	sylanbrc	$⊢ φ \to ({2^{nd} ↾}_{U}) : U \underset{1-1}{⟶} A$

Metamath Proof Explorer

Theorem 2ndresdju

Proof