Theorem 2ndresdju 32653

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 7951	. . . . 5 ⊢ 2nd :V–onto→V
2		fofn 6745	. . . . 5 ⊢ (2nd :V–onto→V → 2nd Fn V)
3	1, 2	mp1i 13	. . . 4 ⊢ (𝜑 → 2nd Fn V)
4		ssv 3955	. . . . 5 ⊢ 𝑈 ⊆ V
5	4	a1i 11	. . . 4 ⊢ (𝜑 → 𝑈 ⊆ V)
6	3, 5	fnssresd 6613	. . 3 ⊢ (𝜑 → (2nd ↾ 𝑈) Fn 𝑈)
7		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝑈)
8	7	fvresd 6851	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢))
9		2ndresdju.u	. . . . . . . 8 ⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)
10		djussxp2 32652	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)
11		2ndresdju.2	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴)
12	11	xpeq2d 5651	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶) = (𝑋 × 𝐴))
13	10, 12	sseqtrid 3973	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴))
14	9, 13	eqsstrid 3969	. . . . . . 7 ⊢ (𝜑 → 𝑈 ⊆ (𝑋 × 𝐴))
15	14	sselda 3930	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ (𝑋 × 𝐴))
16		xp2nd 7963	. . . . . 6 ⊢ (𝑢 ∈ (𝑋 × 𝐴) → (2nd ‘𝑢) ∈ 𝐴)
17	15, 16	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (2nd ‘𝑢) ∈ 𝐴)
18	8, 17	eqeltrd 2833	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴)
19	18	ralrimiva 3125	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴)
20		ffnfv 7061	. . 3 ⊢ ((2nd ↾ 𝑈):𝑈⟶𝐴 ↔ ((2nd ↾ 𝑈) Fn 𝑈 ∧ ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴))
21	6, 19, 20	sylanbrc 583	. 2 ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈⟶𝐴)
22		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑥𝜑
23		nfiu1 4979	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)
24	9, 23	nfcxfr 2893	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑈
25	24	nfcri 2887	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑢 ∈ 𝑈
26	22, 25	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ 𝑈)
27	24	nfcri 2887	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑣 ∈ 𝑈
28	26, 27	nfan 1900	. . . . . . 7 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈)
29		nfcv 2895	. . . . . . . . . 10 ⊢ Ⅎ𝑥2nd
30	29, 24	nfres 5937	. . . . . . . . 9 ⊢ Ⅎ𝑥(2nd ↾ 𝑈)
31		nfcv 2895	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑢
32	30, 31	nffv 6841	. . . . . . . 8 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢)
33		nfcv 2895	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑣
34	30, 33	nffv 6841	. . . . . . . 8 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑣)
35	32, 34	nfeq 2909	. . . . . . 7 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)
36	28, 35	nfan 1900	. . . . . 6 ⊢ Ⅎ𝑥(((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣))
37		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑥 𝑢 = 𝑣
38	9	eleq2i 2825	. . . . . . . 8 ⊢ (𝑢 ∈ 𝑈 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))
39		eliunxp 5783	. . . . . . . 8 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
40	38, 39	sylbb 219	. . . . . . 7 ⊢ (𝑢 ∈ 𝑈 → ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
41	40	ad3antlr 731	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
42	9	eleq2i 2825	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ 𝑈 ↔ 𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))
43		eliunxp 5783	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)))
44	42, 43	bitri 275	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ 𝑈 ↔ ∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)))
45		nfv 1915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶))
46		nfv 1915	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 𝑣 = ⟨𝑦, 𝑑⟩
47		nfv 1915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑦 ∈ 𝑋
48		nfcsb1v 3870	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶
49	48	nfcri 2887	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶
50	47, 49	nfan 1900	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)
51	46, 50	nfan 1900	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
52	51	nfex 2327	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
53		opeq1 4826	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑑⟩ = ⟨𝑦, 𝑑⟩)
54	53	eqeq2d 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑣 = ⟨𝑥, 𝑑⟩ ↔ 𝑣 = ⟨𝑦, 𝑑⟩))
55		eleq1w 2816	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋))
56		csbeq1a 3860	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶)
57	56	eleq2d 2819	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑑 ∈ 𝐶 ↔ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
58	55, 57	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶) ↔ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
59	54, 58	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ (𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))))
60	59	exbidv 1922	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ ∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))))
61	45, 52, 60	cbvexv1 2344	. . . . . . . . . . . 12 ⊢ (∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ ∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
62	44, 61	sylbb 219	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝑈 → ∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
63	62	ad5antlr 735	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → ∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
64		2ndresdju.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶)
65	64	ad9antr 742	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → Disj 𝑥 ∈ 𝑋 𝐶)
66		simp-5r 785	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑥 ∈ 𝑋)
67		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑦 ∈ 𝑋)
68		simp-4r 783	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 ∈ 𝐶)
69		simp-7r 789	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣))
70		simp-9r 793	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 ∈ 𝑈)
71	70	fvresd 6851	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢))
72		simp-6r 787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = ⟨𝑥, 𝑐⟩)
73	72	fveq2d 6835	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = (2nd ‘⟨𝑥, 𝑐⟩))
74		vex 3441	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
75		vex 3441	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑐 ∈ V
76	74, 75	op2nd 7939	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘⟨𝑥, 𝑐⟩) = 𝑐
77	73, 76	eqtrdi 2784	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = 𝑐)
78	71, 77	eqtrd 2768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = 𝑐)
79		simp-8r 791	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 ∈ 𝑈)
80	79	fvresd 6851	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = (2nd ‘𝑣))
81		simpllr 775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 = ⟨𝑦, 𝑑⟩)
82	81	fveq2d 6835	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = (2nd ‘⟨𝑦, 𝑑⟩))
83		vex 3441	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
84		vex 3441	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑑 ∈ V
85	83, 84	op2nd 7939	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘⟨𝑦, 𝑑⟩) = 𝑑
86	82, 85	eqtrdi 2784	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = 𝑑)
87	80, 86	eqtrd 2768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = 𝑑)
88	69, 78, 87	3eqtr3d 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 = 𝑑)
89		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)
90	88, 89	eqeltrd 2833	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶)
91	48, 56	disjif 32579	. . . . . . . . . . . . . . . 16 ⊢ ((Disj 𝑥 ∈ 𝑋 𝐶 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑥 = 𝑦)
92	65, 66, 67, 68, 90, 91	syl122anc 1381	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑥 = 𝑦)
93	92, 88	opeq12d 4834	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ⟨𝑥, 𝑐⟩ = ⟨𝑦, 𝑑⟩)
94	93, 72, 81	3eqtr4d 2778	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = 𝑣)
95	94	anasss 466	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣)
96	95	expl 457	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → ((𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣))
97	96	exlimdvv 1935	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → (∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣))
98	63, 97	mpd 15	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → 𝑢 = 𝑣)
99	98	anasss 466	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣)
100	99	expl 457	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ((𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣))
101	100	exlimdv 1934	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → (∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣))
102	36, 37, 41, 101	exlimimdd 2224	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → 𝑢 = 𝑣)
103	102	ex 412	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
104	103	anasss 466	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
105	104	ralrimivva 3176	. 2 ⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
106		dff13 7197	. 2 ⊢ ((2nd ↾ 𝑈):𝑈–1-1→𝐴 ↔ ((2nd ↾ 𝑈):𝑈⟶𝐴 ∧ ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣)))
107	21, 105, 106	sylanbrc 583	1 ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1→𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∀wral 3048  Vcvv 3437  ⦋csb 3846   ⊆ wss 3898  {csn 4577  ⟨cop 4583  ∪ ciun 4943  Disj wdisj 5062   × cxp 5619   ↾ cres 5623   Fn wfn 6484  ⟶wf 6485  –1-1→wf1 6486  –onto→wfo 6487  ‘cfv 6489  2^nd c2nd 7929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rmo 3347  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-disj 5063  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-fv 6497  df-2nd 7931

This theorem is referenced by:  2ndresdjuf1o  32654  gsumpart  33074