Theorem 2ndresdju 30986

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 7852	. . . . 5 ⊢ 2nd :V–onto→V
2		fofn 6690	. . . . 5 ⊢ (2nd :V–onto→V → 2nd Fn V)
3	1, 2	mp1i 13	. . . 4 ⊢ (𝜑 → 2nd Fn V)
4		ssv 3945	. . . . 5 ⊢ 𝑈 ⊆ V
5	4	a1i 11	. . . 4 ⊢ (𝜑 → 𝑈 ⊆ V)
6	3, 5	fnssresd 6556	. . 3 ⊢ (𝜑 → (2nd ↾ 𝑈) Fn 𝑈)
7		simpr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝑈)
8	7	fvresd 6794	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢))
9		2ndresdju.u	. . . . . . . 8 ⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)
10		djussxp2 30985	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)
11		2ndresdju.2	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴)
12	11	xpeq2d 5619	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶) = (𝑋 × 𝐴))
13	10, 12	sseqtrid 3973	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴))
14	9, 13	eqsstrid 3969	. . . . . . 7 ⊢ (𝜑 → 𝑈 ⊆ (𝑋 × 𝐴))
15	14	sselda 3921	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ (𝑋 × 𝐴))
16		xp2nd 7864	. . . . . 6 ⊢ (𝑢 ∈ (𝑋 × 𝐴) → (2nd ‘𝑢) ∈ 𝐴)
17	15, 16	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (2nd ‘𝑢) ∈ 𝐴)
18	8, 17	eqeltrd 2839	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴)
19	18	ralrimiva 3103	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴)
20		ffnfv 6992	. . 3 ⊢ ((2nd ↾ 𝑈):𝑈⟶𝐴 ↔ ((2nd ↾ 𝑈) Fn 𝑈 ∧ ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴))
21	6, 19, 20	sylanbrc 583	. 2 ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈⟶𝐴)
22		nfv 1917	. . . . . . . . 9 ⊢ Ⅎ𝑥𝜑
23		nfiu1 4958	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)
24	9, 23	nfcxfr 2905	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑈
25	24	nfcri 2894	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑢 ∈ 𝑈
26	22, 25	nfan 1902	. . . . . . . 8 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ 𝑈)
27	24	nfcri 2894	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑣 ∈ 𝑈
28	26, 27	nfan 1902	. . . . . . 7 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈)
29		nfcv 2907	. . . . . . . . . 10 ⊢ Ⅎ𝑥2nd
30	29, 24	nfres 5893	. . . . . . . . 9 ⊢ Ⅎ𝑥(2nd ↾ 𝑈)
31		nfcv 2907	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑢
32	30, 31	nffv 6784	. . . . . . . 8 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢)
33		nfcv 2907	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑣
34	30, 33	nffv 6784	. . . . . . . 8 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑣)
35	32, 34	nfeq 2920	. . . . . . 7 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)
36	28, 35	nfan 1902	. . . . . 6 ⊢ Ⅎ𝑥(((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣))
37		nfv 1917	. . . . . 6 ⊢ Ⅎ𝑥 𝑢 = 𝑣
38	9	eleq2i 2830	. . . . . . . 8 ⊢ (𝑢 ∈ 𝑈 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))
39		eliunxp 5746	. . . . . . . 8 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
40	38, 39	sylbb 218	. . . . . . 7 ⊢ (𝑢 ∈ 𝑈 → ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
41	40	ad3antlr 728	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
42	9	eleq2i 2830	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ 𝑈 ↔ 𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))
43		eliunxp 5746	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)))
44	42, 43	bitri 274	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ 𝑈 ↔ ∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)))
45		nfv 1917	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶))
46		nfv 1917	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 𝑣 = ⟨𝑦, 𝑑⟩
47		nfv 1917	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑦 ∈ 𝑋
48		nfcsb1v 3857	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶
49	48	nfcri 2894	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶
50	47, 49	nfan 1902	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)
51	46, 50	nfan 1902	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
52	51	nfex 2318	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
53		opeq1 4804	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑑⟩ = ⟨𝑦, 𝑑⟩)
54	53	eqeq2d 2749	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑣 = ⟨𝑥, 𝑑⟩ ↔ 𝑣 = ⟨𝑦, 𝑑⟩))
55		eleq1w 2821	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋))
56		csbeq1a 3846	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶)
57	56	eleq2d 2824	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑑 ∈ 𝐶 ↔ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
58	55, 57	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶) ↔ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
59	54, 58	anbi12d 631	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ (𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))))
60	59	exbidv 1924	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ ∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))))
61	45, 52, 60	cbvexv1 2339	. . . . . . . . . . . 12 ⊢ (∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ ∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
62	44, 61	sylbb 218	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝑈 → ∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
63	62	ad5antlr 732	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → ∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
64		2ndresdju.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶)
65	64	ad9antr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → Disj 𝑥 ∈ 𝑋 𝐶)
66		simp-5r 783	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑥 ∈ 𝑋)
67		simplr 766	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑦 ∈ 𝑋)
68		simp-4r 781	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 ∈ 𝐶)
69		simp-7r 787	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣))
70		simp-9r 791	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 ∈ 𝑈)
71	70	fvresd 6794	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢))
72		simp-6r 785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = ⟨𝑥, 𝑐⟩)
73	72	fveq2d 6778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = (2nd ‘⟨𝑥, 𝑐⟩))
74		vex 3436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
75		vex 3436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑐 ∈ V
76	74, 75	op2nd 7840	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘⟨𝑥, 𝑐⟩) = 𝑐
77	73, 76	eqtrdi 2794	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = 𝑐)
78	71, 77	eqtrd 2778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = 𝑐)
79		simp-8r 789	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 ∈ 𝑈)
80	79	fvresd 6794	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = (2nd ‘𝑣))
81		simpllr 773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 = ⟨𝑦, 𝑑⟩)
82	81	fveq2d 6778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = (2nd ‘⟨𝑦, 𝑑⟩))
83		vex 3436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
84		vex 3436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑑 ∈ V
85	83, 84	op2nd 7840	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘⟨𝑦, 𝑑⟩) = 𝑑
86	82, 85	eqtrdi 2794	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = 𝑑)
87	80, 86	eqtrd 2778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = 𝑑)
88	69, 78, 87	3eqtr3d 2786	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 = 𝑑)
89		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)
90	88, 89	eqeltrd 2839	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶)
91	48, 56	disjif 30917	. . . . . . . . . . . . . . . 16 ⊢ ((Disj 𝑥 ∈ 𝑋 𝐶 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑥 = 𝑦)
92	65, 66, 67, 68, 90, 91	syl122anc 1378	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑥 = 𝑦)
93	92, 88	opeq12d 4812	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ⟨𝑥, 𝑐⟩ = ⟨𝑦, 𝑑⟩)
94	93, 72, 81	3eqtr4d 2788	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = 𝑣)
95	94	anasss 467	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣)
96	95	expl 458	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → ((𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣))
97	96	exlimdvv 1937	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → (∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣))
98	63, 97	mpd 15	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → 𝑢 = 𝑣)
99	98	anasss 467	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣)
100	99	expl 458	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ((𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣))
101	100	exlimdv 1936	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → (∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣))
102	36, 37, 41, 101	exlimimdd 2212	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → 𝑢 = 𝑣)
103	102	ex 413	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
104	103	anasss 467	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
105	104	ralrimivva 3123	. 2 ⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
106		dff13 7128	. 2 ⊢ ((2nd ↾ 𝑈):𝑈–1-1→𝐴 ↔ ((2nd ↾ 𝑈):𝑈⟶𝐴 ∧ ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣)))
107	21, 105, 106	sylanbrc 583	1 ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1→𝐴)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106  ∀wral 3064  Vcvv 3432  ⦋csb 3832   ⊆ wss 3887  {csn 4561  ⟨cop 4567  ∪ ciun 4924  Disj wdisj 5039   × cxp 5587   ↾ cres 5591   Fn wfn 6428  ⟶wf 6429  –1-1→wf1 6430  –onto→wfo 6431  ‘cfv 6433  2^nd c2nd 7830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-disj 5040  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-fv 6441  df-2nd 7832

This theorem is referenced by:  2ndresdjuf1o  30987  gsumpart  31315