Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2ndresdju Structured version   Visualization version   GIF version

Theorem 2ndresdju 31117
Description: The 2nd 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.
StepHypRef Expression
1 fo2nd 7898 . . . . 5 2nd :V–onto→V
2 fofn 6727 . . . . 5 (2nd :V–onto→V → 2nd Fn V)
31, 2mp1i 13 . . . 4 (𝜑 → 2nd Fn V)
4 ssv 3954 . . . . 5 𝑈 ⊆ V
54a1i 11 . . . 4 (𝜑𝑈 ⊆ V)
63, 5fnssresd 6594 . . 3 (𝜑 → (2nd𝑈) Fn 𝑈)
7 simpr 485 . . . . . 6 ((𝜑𝑢𝑈) → 𝑢𝑈)
87fvresd 6831 . . . . 5 ((𝜑𝑢𝑈) → ((2nd𝑈)‘𝑢) = (2nd𝑢))
9 2ndresdju.u . . . . . . . 8 𝑈 = 𝑥𝑋 ({𝑥} × 𝐶)
10 djussxp2 31116 . . . . . . . . 9 𝑥𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝑥𝑋 𝐶)
11 2ndresdju.2 . . . . . . . . . 10 (𝜑 𝑥𝑋 𝐶 = 𝐴)
1211xpeq2d 5637 . . . . . . . . 9 (𝜑 → (𝑋 × 𝑥𝑋 𝐶) = (𝑋 × 𝐴))
1310, 12sseqtrid 3982 . . . . . . . 8 (𝜑 𝑥𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴))
149, 13eqsstrid 3978 . . . . . . 7 (𝜑𝑈 ⊆ (𝑋 × 𝐴))
1514sselda 3930 . . . . . 6 ((𝜑𝑢𝑈) → 𝑢 ∈ (𝑋 × 𝐴))
16 xp2nd 7910 . . . . . 6 (𝑢 ∈ (𝑋 × 𝐴) → (2nd𝑢) ∈ 𝐴)
1715, 16syl 17 . . . . 5 ((𝜑𝑢𝑈) → (2nd𝑢) ∈ 𝐴)
188, 17eqeltrd 2837 . . . 4 ((𝜑𝑢𝑈) → ((2nd𝑈)‘𝑢) ∈ 𝐴)
1918ralrimiva 3139 . . 3 (𝜑 → ∀𝑢𝑈 ((2nd𝑈)‘𝑢) ∈ 𝐴)
20 ffnfv 7031 . . 3 ((2nd𝑈):𝑈𝐴 ↔ ((2nd𝑈) Fn 𝑈 ∧ ∀𝑢𝑈 ((2nd𝑈)‘𝑢) ∈ 𝐴))
216, 19, 20sylanbrc 583 . 2 (𝜑 → (2nd𝑈):𝑈𝐴)
22 nfv 1916 . . . . . . . . 9 𝑥𝜑
23 nfiu1 4970 . . . . . . . . . . 11 𝑥 𝑥𝑋 ({𝑥} × 𝐶)
249, 23nfcxfr 2902 . . . . . . . . . 10 𝑥𝑈
2524nfcri 2891 . . . . . . . . 9 𝑥 𝑢𝑈
2622, 25nfan 1901 . . . . . . . 8 𝑥(𝜑𝑢𝑈)
2724nfcri 2891 . . . . . . . 8 𝑥 𝑣𝑈
2826, 27nfan 1901 . . . . . . 7 𝑥((𝜑𝑢𝑈) ∧ 𝑣𝑈)
29 nfcv 2904 . . . . . . . . . 10 𝑥2nd
3029, 24nfres 5912 . . . . . . . . 9 𝑥(2nd𝑈)
31 nfcv 2904 . . . . . . . . 9 𝑥𝑢
3230, 31nffv 6821 . . . . . . . 8 𝑥((2nd𝑈)‘𝑢)
33 nfcv 2904 . . . . . . . . 9 𝑥𝑣
3430, 33nffv 6821 . . . . . . . 8 𝑥((2nd𝑈)‘𝑣)
3532, 34nfeq 2917 . . . . . . 7 𝑥((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)
3628, 35nfan 1901 . . . . . 6 𝑥(((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣))
37 nfv 1916 . . . . . 6 𝑥 𝑢 = 𝑣
389eleq2i 2828 . . . . . . . 8 (𝑢𝑈𝑢 𝑥𝑋 ({𝑥} × 𝐶))
39 eliunxp 5766 . . . . . . . 8 (𝑢 𝑥𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)))
4038, 39sylbb 218 . . . . . . 7 (𝑢𝑈 → ∃𝑥𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)))
4140ad3antlr 728 . . . . . 6 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → ∃𝑥𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)))
429eleq2i 2828 . . . . . . . . . . . . 13 (𝑣𝑈𝑣 𝑥𝑋 ({𝑥} × 𝐶))
43 eliunxp 5766 . . . . . . . . . . . . 13 (𝑣 𝑥𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)))
4442, 43bitri 274 . . . . . . . . . . . 12 (𝑣𝑈 ↔ ∃𝑥𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)))
45 nfv 1916 . . . . . . . . . . . . 13 𝑦𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶))
46 nfv 1916 . . . . . . . . . . . . . . 15 𝑥 𝑣 = ⟨𝑦, 𝑑
47 nfv 1916 . . . . . . . . . . . . . . . 16 𝑥 𝑦𝑋
48 nfcsb1v 3866 . . . . . . . . . . . . . . . . 17 𝑥𝑦 / 𝑥𝐶
4948nfcri 2891 . . . . . . . . . . . . . . . 16 𝑥 𝑑𝑦 / 𝑥𝐶
5047, 49nfan 1901 . . . . . . . . . . . . . . 15 𝑥(𝑦𝑋𝑑𝑦 / 𝑥𝐶)
5146, 50nfan 1901 . . . . . . . . . . . . . 14 𝑥(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))
5251nfex 2317 . . . . . . . . . . . . 13 𝑥𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))
53 opeq1 4814 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ⟨𝑥, 𝑑⟩ = ⟨𝑦, 𝑑⟩)
5453eqeq2d 2747 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑣 = ⟨𝑥, 𝑑⟩ ↔ 𝑣 = ⟨𝑦, 𝑑⟩))
55 eleq1w 2819 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥𝑋𝑦𝑋))
56 csbeq1a 3855 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦𝐶 = 𝑦 / 𝑥𝐶)
5756eleq2d 2822 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑑𝐶𝑑𝑦 / 𝑥𝐶))
5855, 57anbi12d 631 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑥𝑋𝑑𝐶) ↔ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)))
5954, 58anbi12d 631 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)) ↔ (𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))))
6059exbidv 1923 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)) ↔ ∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))))
6145, 52, 60cbvexv1 2338 . . . . . . . . . . . 12 (∃𝑥𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)) ↔ ∃𝑦𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)))
6244, 61sylbb 218 . . . . . . . . . . 11 (𝑣𝑈 → ∃𝑦𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)))
6362ad5antlr 732 . . . . . . . . . 10 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → ∃𝑦𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)))
64 2ndresdju.1 . . . . . . . . . . . . . . . . 17 (𝜑Disj 𝑥𝑋 𝐶)
6564ad9antr 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𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑢𝑈)
7170fvresd 6831 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑢) = (2nd𝑢))
72 simp-6r 785 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑢 = ⟨𝑥, 𝑐⟩)
7372fveq2d 6815 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑢) = (2nd ‘⟨𝑥, 𝑐⟩))
74 vex 3444 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
75 vex 3444 . . . . . . . . . . . . . . . . . . . . 21 𝑐 ∈ V
7674, 75op2nd 7886 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘⟨𝑥, 𝑐⟩) = 𝑐
7773, 76eqtrdi 2792 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑢) = 𝑐)
7871, 77eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑢) = 𝑐)
79 simp-8r 789 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑣𝑈)
8079fvresd 6831 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑣) = (2nd𝑣))
81 simpllr 773 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑣 = ⟨𝑦, 𝑑⟩)
8281fveq2d 6815 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑣) = (2nd ‘⟨𝑦, 𝑑⟩))
83 vex 3444 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
84 vex 3444 . . . . . . . . . . . . . . . . . . . . 21 𝑑 ∈ V
8583, 84op2nd 7886 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘⟨𝑦, 𝑑⟩) = 𝑑
8682, 85eqtrdi 2792 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑣) = 𝑑)
8780, 86eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑣) = 𝑑)
8869, 78, 873eqtr3d 2784 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑐 = 𝑑)
89 simpr 485 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑑𝑦 / 𝑥𝐶)
9088, 89eqeltrd 2837 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑐𝑦 / 𝑥𝐶)
9148, 56disjif 31048 . . . . . . . . . . . . . . . 16 ((Disj 𝑥𝑋 𝐶 ∧ (𝑥𝑋𝑦𝑋) ∧ (𝑐𝐶𝑐𝑦 / 𝑥𝐶)) → 𝑥 = 𝑦)
9265, 66, 67, 68, 90, 91syl122anc 1378 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑥 = 𝑦)
9392, 88opeq12d 4822 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ⟨𝑥, 𝑐⟩ = ⟨𝑦, 𝑑⟩)
9493, 72, 813eqtr4d 2786 . . . . . . . . . . . . 13 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑢 = 𝑣)
9594anasss 467 . . . . . . . . . . . 12 (((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)) → 𝑢 = 𝑣)
9695expl 458 . . . . . . . . . . 11 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → ((𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)) → 𝑢 = 𝑣))
9796exlimdvv 1936 . . . . . . . . . 10 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → (∃𝑦𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)) → 𝑢 = 𝑣))
9863, 97mpd 15 . . . . . . . . 9 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → 𝑢 = 𝑣)
9998anasss 467 . . . . . . . 8 ((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ (𝑥𝑋𝑐𝐶)) → 𝑢 = 𝑣)
10099expl 458 . . . . . . 7 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → ((𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)) → 𝑢 = 𝑣))
101100exlimdv 1935 . . . . . 6 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → (∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)) → 𝑢 = 𝑣))
10236, 37, 41, 101exlimimdd 2211 . . . . 5 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → 𝑢 = 𝑣)
103102ex 413 . . . 4 (((𝜑𝑢𝑈) ∧ 𝑣𝑈) → (((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣) → 𝑢 = 𝑣))
104103anasss 467 . . 3 ((𝜑 ∧ (𝑢𝑈𝑣𝑈)) → (((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣) → 𝑢 = 𝑣))
105104ralrimivva 3193 . 2 (𝜑 → ∀𝑢𝑈𝑣𝑈 (((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣) → 𝑢 = 𝑣))
106 dff13 7167 . 2 ((2nd𝑈):𝑈1-1𝐴 ↔ ((2nd𝑈):𝑈𝐴 ∧ ∀𝑢𝑈𝑣𝑈 (((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣) → 𝑢 = 𝑣)))
10721, 105, 106sylanbrc 583 1 (𝜑 → (2nd𝑈):𝑈1-1𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1540  wex 1780  wcel 2105  wral 3061  Vcvv 3440  csb 3841  wss 3896  {csn 4570  cop 4576   ciun 4936  Disj wdisj 5051   × cxp 5605  cres 5609   Fn wfn 6460  wf 6461  1-1wf1 6462  ontowfo 6463  cfv 6465  2nd c2nd 7876
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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366  ax-un 7629
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3349  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-iun 4938  df-disj 5052  df-br 5087  df-opab 5149  df-mpt 5170  df-id 5506  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-fv 6473  df-2nd 7878
This theorem is referenced by:  2ndresdjuf1o  31118  gsumpart  31446
  Copyright terms: Public domain W3C validator