2ndresdju

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

	Ref	Expression
Hypotheses	2ndresdju.u	⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 )
	2ndresdju.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	2ndresdju.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
	2ndresdju.1	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝑋 𝐶 )
	2ndresdju.2	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴 )
Assertion	2ndresdju	⊢ ( 𝜑 → ( 2^nd ↾ 𝑈 ) : 𝑈 –1-1→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		2ndresdju.u	⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 )
2		2ndresdju.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		2ndresdju.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
4		2ndresdju.1	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝑋 𝐶 )
5		2ndresdju.2	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴 )
6		fo2nd	⊢ 2^nd : V –onto→ V
7		fofn	⊢ ( 2^nd : V –onto→ V → 2^nd Fn V )
8	6 7	mp1i	⊢ ( 𝜑 → 2^nd Fn V )
9		ssv	⊢ 𝑈 ⊆ V
10	9	a1i	⊢ ( 𝜑 → 𝑈 ⊆ V )
11	8 10	fnssresd	⊢ ( 𝜑 → ( 2^nd ↾ 𝑈 ) Fn 𝑈 )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ 𝑈 )
13	12	fvresd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( 2^nd ‘ 𝑢 ) )
14		djussxp2	⊢ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 )
15	5	xpeq2d	⊢ ( 𝜑 → ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) = ( 𝑋 × 𝐴 ) )
16	14 15	sseqtrid	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ ( 𝑋 × 𝐴 ) )
17	1 16	eqsstrid	⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑋 × 𝐴 ) )
18	17	sselda	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ ( 𝑋 × 𝐴 ) )
19		xp2nd	⊢ ( 𝑢 ∈ ( 𝑋 × 𝐴 ) → ( 2^nd ‘ 𝑢 ) ∈ 𝐴 )
20	18 19	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 2^nd ‘ 𝑢 ) ∈ 𝐴 )
21	13 20	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) ∈ 𝐴 )
22	21	ralrimiva	⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑈 ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) ∈ 𝐴 )
23		ffnfv	⊢ ( ( 2^nd ↾ 𝑈 ) : 𝑈 ⟶ 𝐴 ↔ ( ( 2^nd ↾ 𝑈 ) Fn 𝑈 ∧ ∀ 𝑢 ∈ 𝑈 ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) ∈ 𝐴 ) )
24	11 22 23	sylanbrc	⊢ ( 𝜑 → ( 2^nd ↾ 𝑈 ) : 𝑈 ⟶ 𝐴 )
25		nfv	⊢ Ⅎ 𝑥 𝜑
26		nfiu1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 )
27	1 26	nfcxfr	⊢ Ⅎ 𝑥 𝑈
28	27	nfcri	⊢ Ⅎ 𝑥 𝑢 ∈ 𝑈
29	25 28	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑢 ∈ 𝑈 )
30	27	nfcri	⊢ Ⅎ 𝑥 𝑣 ∈ 𝑈
31	29 30	nfan	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 )
32		nfcv	⊢ Ⅎ 𝑥 2^nd
33	32 27	nfres	⊢ Ⅎ 𝑥 ( 2^nd ↾ 𝑈 )
34		nfcv	⊢ Ⅎ 𝑥 𝑢
35	33 34	nffv	⊢ Ⅎ 𝑥 ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 )
36		nfcv	⊢ Ⅎ 𝑥 𝑣
37	33 36	nffv	⊢ Ⅎ 𝑥 ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 )
38	35 37	nfeq	⊢ Ⅎ 𝑥 ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 )
39	31 38	nfan	⊢ Ⅎ 𝑥 ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) )
40		nfv	⊢ Ⅎ 𝑥 𝑢 = 𝑣
41	1	eleq2i	⊢ ( 𝑢 ∈ 𝑈 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) )
42		eliunxp	⊢ ( 𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑐 ( 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶 ) ) )
43	41 42	sylbb	⊢ ( 𝑢 ∈ 𝑈 → ∃ 𝑥 ∃ 𝑐 ( 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶 ) ) )
44	43	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) → ∃ 𝑥 ∃ 𝑐 ( 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶 ) ) )
45	1	eleq2i	⊢ ( 𝑣 ∈ 𝑈 ↔ 𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) )
46		eliunxp	⊢ ( 𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑑 ( 𝑣 = ⟨ 𝑥 , 𝑑 ⟩ ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶 ) ) )
47	45 46	bitri	⊢ ( 𝑣 ∈ 𝑈 ↔ ∃ 𝑥 ∃ 𝑑 ( 𝑣 = ⟨ 𝑥 , 𝑑 ⟩ ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶 ) ) )
48		nfv	⊢ Ⅎ 𝑦 ∃ 𝑑 ( 𝑣 = ⟨ 𝑥 , 𝑑 ⟩ ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶 ) )
49		nfv	⊢ Ⅎ 𝑥 𝑣 = ⟨ 𝑦 , 𝑑 ⟩
50		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝑋
51		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
52	51	nfcri	⊢ Ⅎ 𝑥 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶
53	50 52	nfan	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
54	49 53	nfan	⊢ Ⅎ 𝑥 ( 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
55	54	nfex	⊢ Ⅎ 𝑥 ∃ 𝑑 ( 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
56		opeq1	⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑑 ⟩ = ⟨ 𝑦 , 𝑑 ⟩ )
57	56	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑣 = ⟨ 𝑥 , 𝑑 ⟩ ↔ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) )
58		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋 ) )
59		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
60	59	eleq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑑 ∈ 𝐶 ↔ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
61	58 60	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶 ) ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
62	57 61	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑣 = ⟨ 𝑥 , 𝑑 ⟩ ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶 ) ) ↔ ( 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ) )
63	62	exbidv	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑑 ( 𝑣 = ⟨ 𝑥 , 𝑑 ⟩ ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶 ) ) ↔ ∃ 𝑑 ( 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ) )
64	48 55 63	cbvexv1	⊢ ( ∃ 𝑥 ∃ 𝑑 ( 𝑣 = ⟨ 𝑥 , 𝑑 ⟩ ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ∃ 𝑑 ( 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
65	47 64	sylbb	⊢ ( 𝑣 ∈ 𝑈 → ∃ 𝑦 ∃ 𝑑 ( 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
66	65	ad5antlr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) → ∃ 𝑦 ∃ 𝑑 ( 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
67	4	ad9antr	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → Disj 𝑥 ∈ 𝑋 𝐶 )
68		simp-5r	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → 𝑥 ∈ 𝑋 )
69		simplr	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → 𝑦 ∈ 𝑋 )
70		simp-4r	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → 𝑐 ∈ 𝐶 )
71		simp-7r	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) )
72		simp-9r	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → 𝑢 ∈ 𝑈 )
73	72	fvresd	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( 2^nd ‘ 𝑢 ) )
74		simp-6r	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ )
75	74	fveq2d	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ ⟨ 𝑥 , 𝑐 ⟩ ) )
76		vex	⊢ 𝑥 ∈ V
77		vex	⊢ 𝑐 ∈ V
78	76 77	op2nd	⊢ ( 2^nd ‘ ⟨ 𝑥 , 𝑐 ⟩ ) = 𝑐
79	75 78	eqtrdi	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → ( 2^nd ‘ 𝑢 ) = 𝑐 )
80	73 79	eqtrd	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = 𝑐 )
81		simp-8r	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → 𝑣 ∈ 𝑈 )
82	81	fvresd	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) = ( 2^nd ‘ 𝑣 ) )
83		simpllr	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ )
84	83	fveq2d	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → ( 2^nd ‘ 𝑣 ) = ( 2^nd ‘ ⟨ 𝑦 , 𝑑 ⟩ ) )
85		vex	⊢ 𝑦 ∈ V
86		vex	⊢ 𝑑 ∈ V
87	85 86	op2nd	⊢ ( 2^nd ‘ ⟨ 𝑦 , 𝑑 ⟩ ) = 𝑑
88	84 87	eqtrdi	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → ( 2^nd ‘ 𝑣 ) = 𝑑 )
89	82 88	eqtrd	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) = 𝑑 )
90	71 80 89	3eqtr3d	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → 𝑐 = 𝑑 )
91		simpr	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
92	90 91	eqeltrd	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → 𝑐 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
93	51 59	disjif	⊢ ( ( Disj 𝑥 ∈ 𝑋 𝐶 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑐 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) → 𝑥 = 𝑦 )
94	67 68 69 70 92 93	syl122anc	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → 𝑥 = 𝑦 )
95	94 90	opeq12d	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → ⟨ 𝑥 , 𝑐 ⟩ = ⟨ 𝑦 , 𝑑 ⟩ )
96	95 74 83	3eqtr4d	⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → 𝑢 = 𝑣 )
97	96	anasss	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) → 𝑢 = 𝑣 )
98	97	expl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) → 𝑢 = 𝑣 ) )
99	98	exlimdvv	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) → ( ∃ 𝑦 ∃ 𝑑 ( 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) → 𝑢 = 𝑣 ) )
100	66 99	mpd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝐶 ) → 𝑢 = 𝑣 )
101	100	anasss	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑢 = 𝑣 )
102	101	expl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) → ( ( 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑢 = 𝑣 ) )
103	102	exlimdv	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) → ( ∃ 𝑐 ( 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑢 = 𝑣 ) )
104	39 40 44 103	exlimimdd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) ) → 𝑢 = 𝑣 )
105	104	ex	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) → ( ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
106	105	anasss	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ) ) → ( ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
107	106	ralrimivva	⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑈 ∀ 𝑣 ∈ 𝑈 ( ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
108		dff13	⊢ ( ( 2^nd ↾ 𝑈 ) : 𝑈 –1-1→ 𝐴 ↔ ( ( 2^nd ↾ 𝑈 ) : 𝑈 ⟶ 𝐴 ∧ ∀ 𝑢 ∈ 𝑈 ∀ 𝑣 ∈ 𝑈 ( ( ( 2^nd ↾ 𝑈 ) ‘ 𝑢 ) = ( ( 2^nd ↾ 𝑈 ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ) )
109	24 107 108	sylanbrc	⊢ ( 𝜑 → ( 2^nd ↾ 𝑈 ) : 𝑈 –1-1→ 𝐴 )

Metamath Proof Explorer

Theorem 2ndresdju

Proof