Theorem 2ndresdju 30494

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 7707	. . . . 5 ⊢ 2nd :V–onto→V
2		fofn 6571	. . . . 5 ⊢ (2nd :V–onto→V → 2nd Fn V)
3	1, 2	mp1i 13	. . . 4 ⊢ (𝜑 → 2nd Fn V)
4		ssv 3912	. . . . 5 ⊢ 𝑈 ⊆ V
5	4	a1i 11	. . . 4 ⊢ (𝜑 → 𝑈 ⊆ V)
6	3, 5	fnssresd 6447	. . 3 ⊢ (𝜑 → (2nd ↾ 𝑈) Fn 𝑈)
7		simpr 489	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝑈)
8	7	fvresd 6671	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢))
9		2ndresdju.u	. . . . . . . 8 ⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)
10		djussxp2 30493	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)
11		2ndresdju.2	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴)
12	11	xpeq2d 5547	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶) = (𝑋 × 𝐴))
13	10, 12	sseqtrid 3940	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴))
14	9, 13	eqsstrid 3936	. . . . . . 7 ⊢ (𝜑 → 𝑈 ⊆ (𝑋 × 𝐴))
15	14	sselda 3888	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ (𝑋 × 𝐴))
16		xp2nd 7719	. . . . . 6 ⊢ (𝑢 ∈ (𝑋 × 𝐴) → (2nd ‘𝑢) ∈ 𝐴)
17	15, 16	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (2nd ‘𝑢) ∈ 𝐴)
18	8, 17	eqeltrd 2851	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴)
19	18	ralrimiva 3111	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴)
20		ffnfv 6866	. . 3 ⊢ ((2nd ↾ 𝑈):𝑈⟶𝐴 ↔ ((2nd ↾ 𝑈) Fn 𝑈 ∧ ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴))
21	6, 19, 20	sylanbrc 587	. 2 ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈⟶𝐴)
22		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑥𝜑
23		nfiu1 4910	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)
24	9, 23	nfcxfr 2915	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑈
25	24	nfcri 2904	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑢 ∈ 𝑈
26	22, 25	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ 𝑈)
27	24	nfcri 2904	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑣 ∈ 𝑈
28	26, 27	nfan 1901	. . . . . . 7 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈)
29		nfcv 2917	. . . . . . . . . 10 ⊢ Ⅎ𝑥2nd
30	29, 24	nfres 5818	. . . . . . . . 9 ⊢ Ⅎ𝑥(2nd ↾ 𝑈)
31		nfcv 2917	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑢
32	30, 31	nffv 6661	. . . . . . . 8 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢)
33		nfcv 2917	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑣
34	30, 33	nffv 6661	. . . . . . . 8 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑣)
35	32, 34	nfeq 2930	. . . . . . 7 ⊢ Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)
36	28, 35	nfan 1901	. . . . . 6 ⊢ Ⅎ𝑥(((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣))
37		nfv 1916	. . . . . 6 ⊢ Ⅎ𝑥 𝑢 = 𝑣
38	9	eleq2i 2842	. . . . . . . 8 ⊢ (𝑢 ∈ 𝑈 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))
39		eliunxp 5670	. . . . . . . 8 ⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
40	38, 39	sylbb 222	. . . . . . 7 ⊢ (𝑢 ∈ 𝑈 → ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
41	40	ad3antlr 731	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ∃𝑥∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)))
42	9	eleq2i 2842	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ 𝑈 ↔ 𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))
43		eliunxp 5670	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)))
44	42, 43	bitri 278	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ 𝑈 ↔ ∃𝑥∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)))
45		nfv 1916	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶))
46		nfv 1916	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 𝑣 = ⟨𝑦, 𝑑⟩
47		nfv 1916	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑦 ∈ 𝑋
48		nfcsb1v 3825	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶
49	48	nfcri 2904	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶
50	47, 49	nfan 1901	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)
51	46, 50	nfan 1901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
52	51	nfex 2333	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
53		opeq1 4754	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑑⟩ = ⟨𝑦, 𝑑⟩)
54	53	eqeq2d 2770	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑣 = ⟨𝑥, 𝑑⟩ ↔ 𝑣 = ⟨𝑦, 𝑑⟩))
55		eleq1w 2833	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋))
56		csbeq1a 3815	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶)
57	56	eleq2d 2836	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑑 ∈ 𝐶 ↔ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))
58	55, 57	anbi12d 634	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶) ↔ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
59	54, 58	anbi12d 634	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ (𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))))
60	59	exbidv 1923	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ ∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))))
61	45, 52, 60	cbvexv1 2352	. . . . . . . . . . . 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 6671	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢))
72		simp-6r 788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = ⟨𝑥, 𝑐⟩)
73	72	fveq2d 6655	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = (2nd ‘⟨𝑥, 𝑐⟩))
74		vex 3411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
75		vex 3411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑐 ∈ V
76	74, 75	op2nd 7695	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘⟨𝑥, 𝑐⟩) = 𝑐
77	73, 76	eqtrdi 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = 𝑐)
78	71, 77	eqtrd 2794	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = 𝑐)
79		simp-8r 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 ∈ 𝑈)
80	79	fvresd 6671	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = (2nd ‘𝑣))
81		simpllr 776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 = ⟨𝑦, 𝑑⟩)
82	81	fveq2d 6655	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = (2nd ‘⟨𝑦, 𝑑⟩))
83		vex 3411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
84		vex 3411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑑 ∈ V
85	83, 84	op2nd 7695	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘⟨𝑦, 𝑑⟩) = 𝑑
86	82, 85	eqtrdi 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = 𝑑)
87	80, 86	eqtrd 2794	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = 𝑑)
88	69, 78, 87	3eqtr3d 2802	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 = 𝑑)
89		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)
90	88, 89	eqeltrd 2851	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶)
91	48, 56	disjif 30424	. . . . . . . . . . . . . . . 16 ⊢ ((Disj 𝑥 ∈ 𝑋 𝐶 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑥 = 𝑦)
92	65, 66, 67, 68, 90, 91	syl122anc 1377	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑥 = 𝑦)
93	92, 88	opeq12d 4764	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ⟨𝑥, 𝑐⟩ = ⟨𝑦, 𝑑⟩)
94	93, 72, 81	3eqtr4d 2804	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = 𝑣)
95	94	anasss 471	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣)
96	95	expl 462	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → ((𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣))
97	96	exlimdvv 1936	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → (∃𝑦∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣))
98	63, 97	mpd 15	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → 𝑢 = 𝑣)
99	98	anasss 471	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣)
100	99	expl 462	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ((𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣))
101	100	exlimdv 1935	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → (∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣))
102	36, 37, 41, 101	exlimimdd 2218	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → 𝑢 = 𝑣)
103	102	ex 417	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
104	103	anasss 471	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
105	104	ralrimivva 3118	. 2 ⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))
106		dff13 6998	. 2 ⊢ ((2nd ↾ 𝑈):𝑈–1-1→𝐴 ↔ ((2nd ↾ 𝑈):𝑈⟶𝐴 ∧ ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣)))
107	21, 105, 106	sylanbrc 587	1 ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1→𝐴)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539  ∃wex 1782   ∈ wcel 2112  ∀wral 3068  Vcvv 3407  ⦋csb 3801   ⊆ wss 3854  {csn 4515  ⟨cop 4521  ∪ ciun 4876  Disj wdisj 4990   × cxp 5515   ↾ cres 5519   Fn wfn 6323  ⟶wf 6324  –1-1→wf1 6325  –onto→wfo 6326  ‘cfv 6328  2^nd c2nd 7685

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5162  ax-nul 5169  ax-pr 5291  ax-un 7452

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-ral 3073  df-rex 3074  df-rmo 3076  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-nul 4222  df-if 4414  df-sn 4516  df-pr 4518  df-op 4522  df-uni 4792  df-iun 4878  df-disj 4991  df-br 5026  df-opab 5088  df-mpt 5106  df-id 5423  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-fv 6336  df-2nd 7687

This theorem is referenced by:  2ndresdjuf1o  30495  gsumpart  30826