Theorem 2ndresdju 32975

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

Hypotheses

Ref	Expression
2ndresdju.u	⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)
2ndresdju.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
2ndresdju.x	⊢ (𝜑 → 𝑋 ∈ 𝑊)
2ndresdju.1	⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶)
2ndresdju.2	⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴)

Assertion

Ref	Expression
2ndresdju	⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1→𝐴)

Distinct variable groups:   𝑥,𝐴   𝑥,𝑋   𝜑,𝑥

Allowed substitution hints:   𝐶(𝑥)   𝑈(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem 2ndresdju

Dummy variables 𝑢 𝑐 𝑑 𝑦 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fo2nd 8008	. . . . 5 ⊢ 2nd :V–onto→V
2		fofn 6796	. . . . 5 ⊢ (2nd :V–onto→V → 2nd Fn V)
3	1, 2	mp1i 14	. . . 4 ⊢ (𝜑 → 2nd Fn V)
4		ssv 3962	. . . . 5 ⊢ 𝑈 ⊆ V
5	4	a1i 11	. . . 4 ⊢ (𝜑 → 𝑈 ⊆ V)
6	3, 5	fnssresd 6661	. . 3 ⊢ (𝜑 → (2nd ↾ 𝑈) Fn 𝑈)
7		simpr 489	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝑈)
8	7	fvresd 6903	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢))
9		2ndresdju.u	. . . . . . . 8 ⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)
10		djussxp2 32974	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)
11		2ndresdju.2	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴)
12	11	xpeq2d 5693	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶) = (𝑋 × 𝐴))
13	10, 12	sseqtrid 3980	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴))
14	9, 13	eqsstrid 3976	. . . . . . 7 ⊢ (𝜑 → 𝑈 ⊆ (𝑋 × 𝐴))
15	14	sselda 3938	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ (𝑋 × 𝐴))
16		xp2nd 8020	. . . . . 6 ⊢ (𝑢 ∈ (𝑋 × 𝐴) → (2nd ‘𝑢) ∈ 𝐴)
17	15, 16	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (2nd ‘𝑢) ∈ 𝐴)
18	8, 17	eqeltrd 2863	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴)
19	18	ralrimiva 3157	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴)
20		ffnfv 7116	. . 3 ⊢ ((2nd ↾ 𝑈):𝑈⟶𝐴 ↔ ((2nd ↾ 𝑈) Fn 𝑈 ∧ ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴))
21	6, 19, 20	sylanbrc 594	. 2 ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈⟶𝐴)
22		nfv 1944	. . . . . . . . 9 ⊢ Ⅎ𝑥𝜑
23		nfiu1 4993	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)
24	9, 23	nfcxfr 2923	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑈
25	24	nfcri 2917	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑢 ∈ 𝑈
26	22, 25	nfan 1929	. . . . . . . 8 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ 𝑈)
27	24	nfcri 2917	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑣 ∈ 𝑈
28	26, 27	nfan 1929	. . . . . . 7 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈)
29		nfcv 2925	. . . . . . . . . 10 ⊢ Ⅎ𝑥2nd
30	29, 24	nfres 5982	. . . . . . . . 9 ⊢ Ⅎ𝑥(2nd ↾ 𝑈)
31		nfcv 2925	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑢
32	30, 31	nffv 6893	. . . . . . . 8 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢)
33		nfcv 2925	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑣
34	30, 33	nffv 6893	. . . . . . . 8 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑣)
35	32, 34	nfeq 2938	. . . . . . 7 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)
36	28, 35	nfan 1929	. . . . . 6 ⊢ Ⅎ𝑥(((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣))
37		nfv 1944	. . . . . 6 ⊢ Ⅎ𝑥 𝑢 = 𝑣
38	9	eleq2i 2855	. . . . . . . 8 ⊢ (𝑢 ∈ 𝑈 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))
39		eliunxp 5825	. . . . . . . 8 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
40	38, 39	sylbb 222	. . . . . . 7 ⊢ (𝑢 ∈ 𝑈 → ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
41	40	ad3antlr 743	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
42	9	eleq2i 2855	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ 𝑈 ↔ 𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))
43		eliunxp 5825	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)))
44	42, 43	bitri 278	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ 𝑈 ↔ ∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)))
45		nfv 1944	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶))
46		nfv 1944	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 𝑣 = ⟨𝑦, 𝑑⟩
47		nfv 1944	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑦 ∈ 𝑋
48		nfcsb1v 3878	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶
49	48	nfcri 2917	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶
50	47, 49	nfan 1929	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)
51	46, 50	nfan 1929	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
52	51	nfex 2357	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
53		opeq1 4839	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑑⟩ = ⟨𝑦, 𝑑⟩)
54	53	eqeq2d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑣 = ⟨𝑥, 𝑑⟩ ↔ 𝑣 = ⟨𝑦, 𝑑⟩))
55		eleq1w 2846	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋))
56		csbeq1a 3868	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶)
57	56	eleq2d 2849	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑑 ∈ 𝐶 ↔ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
58	55, 57	anbi12d 643	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶) ↔ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
59	54, 58	anbi12d 643	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ (𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))))
60	59	exbidv 1951	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ ∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))))
61	45, 52, 60	cbvexv1 2374	. . . . . . . . . . . 12 ⊢ (∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ ∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
62	44, 61	sylbb 222	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝑈 → ∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
63	62	ad5antlr 747	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → ∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
64		2ndresdju.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶)
65	64	ad9antr 754	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → Disj 𝑥 ∈ 𝑋 𝐶)
66		simp-5r 797	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑥 ∈ 𝑋)
67		simplr 780	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑦 ∈ 𝑋)
68		simp-4r 795	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 ∈ 𝐶)
69		simp-7r 801	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣))
70		simp-9r 805	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 ∈ 𝑈)
71	70	fvresd 6903	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢))
72		simp-6r 799	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = ⟨𝑥, 𝑐⟩)
73	72	fveq2d 6887	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = (2nd ‘⟨𝑥, 𝑐⟩))
74		vex 3459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
75		vex 3459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑐 ∈ V
76	74, 75	op2nd 7996	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘⟨𝑥, 𝑐⟩) = 𝑐
77	73, 76	eqtrdi 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = 𝑐)
78	71, 77	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = 𝑐)
79		simp-8r 803	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 ∈ 𝑈)
80	79	fvresd 6903	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = (2nd ‘𝑣))
81		simpllr 787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 = ⟨𝑦, 𝑑⟩)
82	81	fveq2d 6887	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = (2nd ‘⟨𝑦, 𝑑⟩))
83		vex 3459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
84		vex 3459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑑 ∈ V
85	83, 84	op2nd 7996	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘⟨𝑦, 𝑑⟩) = 𝑑
86	82, 85	eqtrdi 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = 𝑑)
87	80, 86	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = 𝑑)
88	69, 78, 87	3eqtr3d 2806	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 = 𝑑)
89		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)
90	88, 89	eqeltrd 2863	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶)
91	48, 56	disjif 32904	. . . . . . . . . . . . . . . 16 ⊢ ((Disj 𝑥 ∈ 𝑋 𝐶 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑥 = 𝑦)
92	65, 66, 67, 68, 90, 91	syl122anc 1406	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑥 = 𝑦)
93	92, 88	opeq12d 4847	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ⟨𝑥, 𝑐⟩ = ⟨𝑦, 𝑑⟩)
94	93, 72, 81	3eqtr4d 2808	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = 𝑣)
95	94	anasss 471	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣)
96	95	expl 462	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → ((𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣))
97	96	exlimdvv 1964	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → (∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣))
98	63, 97	mpd 16	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → 𝑢 = 𝑣)
99	98	anasss 471	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣)
100	99	expl 462	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ((𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣))
101	100	exlimdv 1963	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → (∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣))
102	36, 37, 41, 101	exlimimdd 2255	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → 𝑢 = 𝑣)
103	102	ex 417	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
104	103	anasss 471	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
105	104	ralrimivva 3208	. 2 ⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
106		dff13 7254	. 2 ⊢ ((2nd ↾ 𝑈):𝑈–1-1→𝐴 ↔ ((2nd ↾ 𝑈):𝑈⟶𝐴 ∧ ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣)))
107	21, 105, 106	sylanbrc 594	1 ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1→𝐴)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∀wral 3079  Vcvv 3455  ⦋csb 3854   ⊆ wss 3906  {csn 4590  ⟨cop 4596  ∪ ciun 4957  Disj wdisj 5077   × cxp 5661   ↾ cres 5665   Fn wfn 6533  ⟶wf 6534  –1-1→wf1 6535  –onto→wfo 6536  ‘cfv 6538  2^nd c2nd 7986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-disj 5078  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-fv 6546  df-2nd 7988

This theorem is referenced by:  2ndresdjuf1o  32976  gsumpart  33364