Theorem 2ndresdju 30659

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 7760	. . . . 5 ⊢ 2nd :V–onto→V
2		fofn 6613	. . . . 5 ⊢ (2nd :V–onto→V → 2nd Fn V)
3	1, 2	mp1i 13	. . . 4 ⊢ (𝜑 → 2nd Fn V)
4		ssv 3911	. . . . 5 ⊢ 𝑈 ⊆ V
5	4	a1i 11	. . . 4 ⊢ (𝜑 → 𝑈 ⊆ V)
6	3, 5	fnssresd 6479	. . 3 ⊢ (𝜑 → (2nd ↾ 𝑈) Fn 𝑈)
7		simpr 488	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝑈)
8	7	fvresd 6715	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢))
9		2ndresdju.u	. . . . . . . 8 ⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)
10		djussxp2 30658	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)
11		2ndresdju.2	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴)
12	11	xpeq2d 5566	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶) = (𝑋 × 𝐴))
13	10, 12	sseqtrid 3939	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴))
14	9, 13	eqsstrid 3935	. . . . . . 7 ⊢ (𝜑 → 𝑈 ⊆ (𝑋 × 𝐴))
15	14	sselda 3887	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ (𝑋 × 𝐴))
16		xp2nd 7772	. . . . . 6 ⊢ (𝑢 ∈ (𝑋 × 𝐴) → (2nd ‘𝑢) ∈ 𝐴)
17	15, 16	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (2nd ‘𝑢) ∈ 𝐴)
18	8, 17	eqeltrd 2831	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴)
19	18	ralrimiva 3095	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴)
20		ffnfv 6913	. . 3 ⊢ ((2nd ↾ 𝑈):𝑈⟶𝐴 ↔ ((2nd ↾ 𝑈) Fn 𝑈 ∧ ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴))
21	6, 19, 20	sylanbrc 586	. 2 ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈⟶𝐴)
22		nfv 1922	. . . . . . . . 9 ⊢ Ⅎ𝑥𝜑
23		nfiu1 4924	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)
24	9, 23	nfcxfr 2895	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑈
25	24	nfcri 2884	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑢 ∈ 𝑈
26	22, 25	nfan 1907	. . . . . . . 8 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ 𝑈)
27	24	nfcri 2884	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑣 ∈ 𝑈
28	26, 27	nfan 1907	. . . . . . 7 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈)
29		nfcv 2897	. . . . . . . . . 10 ⊢ Ⅎ𝑥2nd
30	29, 24	nfres 5838	. . . . . . . . 9 ⊢ Ⅎ𝑥(2nd ↾ 𝑈)
31		nfcv 2897	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑢
32	30, 31	nffv 6705	. . . . . . . 8 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢)
33		nfcv 2897	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑣
34	30, 33	nffv 6705	. . . . . . . 8 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑣)
35	32, 34	nfeq 2910	. . . . . . 7 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)
36	28, 35	nfan 1907	. . . . . 6 ⊢ Ⅎ𝑥(((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣))
37		nfv 1922	. . . . . 6 ⊢ Ⅎ𝑥 𝑢 = 𝑣
38	9	eleq2i 2822	. . . . . . . 8 ⊢ (𝑢 ∈ 𝑈 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))
39		eliunxp 5691	. . . . . . . 8 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
40	38, 39	sylbb 222	. . . . . . 7 ⊢ (𝑢 ∈ 𝑈 → ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
41	40	ad3antlr 731	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
42	9	eleq2i 2822	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ 𝑈 ↔ 𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))
43		eliunxp 5691	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)))
44	42, 43	bitri 278	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ 𝑈 ↔ ∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)))
45		nfv 1922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶))
46		nfv 1922	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 𝑣 = ⟨𝑦, 𝑑⟩
47		nfv 1922	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑦 ∈ 𝑋
48		nfcsb1v 3823	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶
49	48	nfcri 2884	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶
50	47, 49	nfan 1907	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)
51	46, 50	nfan 1907	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
52	51	nfex 2325	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
53		opeq1 4770	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑑⟩ = ⟨𝑦, 𝑑⟩)
54	53	eqeq2d 2747	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑣 = ⟨𝑥, 𝑑⟩ ↔ 𝑣 = ⟨𝑦, 𝑑⟩))
55		eleq1w 2813	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋))
56		csbeq1a 3812	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶)
57	56	eleq2d 2816	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑑 ∈ 𝐶 ↔ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
58	55, 57	anbi12d 634	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶) ↔ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
59	54, 58	anbi12d 634	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ (𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))))
60	59	exbidv 1929	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ ∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))))
61	45, 52, 60	cbvexv1 2343	. . . . . . . . . . . 12 ⊢ (∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ ∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
62	44, 61	sylbb 222	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝑈 → ∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
63	62	ad5antlr 735	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → ∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
64		2ndresdju.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶)
65	64	ad9antr 742	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → Disj 𝑥 ∈ 𝑋 𝐶)
66		simp-5r 786	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑥 ∈ 𝑋)
67		simplr 769	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑦 ∈ 𝑋)
68		simp-4r 784	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 ∈ 𝐶)
69		simp-7r 790	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣))
70		simp-9r 794	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 ∈ 𝑈)
71	70	fvresd 6715	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢))
72		simp-6r 788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = ⟨𝑥, 𝑐⟩)
73	72	fveq2d 6699	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = (2nd ‘⟨𝑥, 𝑐⟩))
74		vex 3402	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
75		vex 3402	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑐 ∈ V
76	74, 75	op2nd 7748	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘⟨𝑥, 𝑐⟩) = 𝑐
77	73, 76	eqtrdi 2787	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = 𝑐)
78	71, 77	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = 𝑐)
79		simp-8r 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 ∈ 𝑈)
80	79	fvresd 6715	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = (2nd ‘𝑣))
81		simpllr 776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 = ⟨𝑦, 𝑑⟩)
82	81	fveq2d 6699	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = (2nd ‘⟨𝑦, 𝑑⟩))
83		vex 3402	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
84		vex 3402	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑑 ∈ V
85	83, 84	op2nd 7748	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘⟨𝑦, 𝑑⟩) = 𝑑
86	82, 85	eqtrdi 2787	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = 𝑑)
87	80, 86	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = 𝑑)
88	69, 78, 87	3eqtr3d 2779	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 = 𝑑)
89		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)
90	88, 89	eqeltrd 2831	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶)
91	48, 56	disjif 30590	. . . . . . . . . . . . . . . 16 ⊢ ((Disj 𝑥 ∈ 𝑋 𝐶 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑥 = 𝑦)
92	65, 66, 67, 68, 90, 91	syl122anc 1381	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑥 = 𝑦)
93	92, 88	opeq12d 4778	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ⟨𝑥, 𝑐⟩ = ⟨𝑦, 𝑑⟩)
94	93, 72, 81	3eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = 𝑣)
95	94	anasss 470	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣)
96	95	expl 461	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → ((𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣))
97	96	exlimdvv 1942	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → (∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣))
98	63, 97	mpd 15	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → 𝑢 = 𝑣)
99	98	anasss 470	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣)
100	99	expl 461	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ((𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣))
101	100	exlimdv 1941	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → (∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣))
102	36, 37, 41, 101	exlimimdd 2219	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → 𝑢 = 𝑣)
103	102	ex 416	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
104	103	anasss 470	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
105	104	ralrimivva 3102	. 2 ⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
106		dff13 7045	. 2 ⊢ ((2nd ↾ 𝑈):𝑈–1-1→𝐴 ↔ ((2nd ↾ 𝑈):𝑈⟶𝐴 ∧ ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣)))
107	21, 105, 106	sylanbrc 586	1 ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1→𝐴)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543  ∃wex 1787   ∈ wcel 2112  ∀wral 3051  Vcvv 3398  ⦋csb 3798   ⊆ wss 3853  {csn 4527  ⟨cop 4533  ∪ ciun 4890  Disj wdisj 5004   × cxp 5534   ↾ cres 5538   Fn wfn 6353  ⟶wf 6354  –1-1→wf1 6355  –onto→wfo 6356  ‘cfv 6358  2^nd c2nd 7738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-rmo 3059  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-iun 4892  df-disj 5005  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-fv 6366  df-2nd 7740

This theorem is referenced by:  2ndresdjuf1o  30660  gsumpart  30988