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 32666
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 8034 . . . . 5 2nd :V–onto→V
2 fofn 6823 . . . . 5 (2nd :V–onto→V → 2nd Fn V)
31, 2mp1i 13 . . . 4 (𝜑 → 2nd Fn V)
4 ssv 4020 . . . . 5 𝑈 ⊆ V
54a1i 11 . . . 4 (𝜑𝑈 ⊆ V)
63, 5fnssresd 6693 . . 3 (𝜑 → (2nd𝑈) Fn 𝑈)
7 simpr 484 . . . . . 6 ((𝜑𝑢𝑈) → 𝑢𝑈)
87fvresd 6927 . . . . 5 ((𝜑𝑢𝑈) → ((2nd𝑈)‘𝑢) = (2nd𝑢))
9 2ndresdju.u . . . . . . . 8 𝑈 = 𝑥𝑋 ({𝑥} × 𝐶)
10 djussxp2 32665 . . . . . . . . 9 𝑥𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝑥𝑋 𝐶)
11 2ndresdju.2 . . . . . . . . . 10 (𝜑 𝑥𝑋 𝐶 = 𝐴)
1211xpeq2d 5719 . . . . . . . . 9 (𝜑 → (𝑋 × 𝑥𝑋 𝐶) = (𝑋 × 𝐴))
1310, 12sseqtrid 4048 . . . . . . . 8 (𝜑 𝑥𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴))
149, 13eqsstrid 4044 . . . . . . 7 (𝜑𝑈 ⊆ (𝑋 × 𝐴))
1514sselda 3995 . . . . . 6 ((𝜑𝑢𝑈) → 𝑢 ∈ (𝑋 × 𝐴))
16 xp2nd 8046 . . . . . 6 (𝑢 ∈ (𝑋 × 𝐴) → (2nd𝑢) ∈ 𝐴)
1715, 16syl 17 . . . . 5 ((𝜑𝑢𝑈) → (2nd𝑢) ∈ 𝐴)
188, 17eqeltrd 2839 . . . 4 ((𝜑𝑢𝑈) → ((2nd𝑈)‘𝑢) ∈ 𝐴)
1918ralrimiva 3144 . . 3 (𝜑 → ∀𝑢𝑈 ((2nd𝑈)‘𝑢) ∈ 𝐴)
20 ffnfv 7139 . . 3 ((2nd𝑈):𝑈𝐴 ↔ ((2nd𝑈) Fn 𝑈 ∧ ∀𝑢𝑈 ((2nd𝑈)‘𝑢) ∈ 𝐴))
216, 19, 20sylanbrc 583 . 2 (𝜑 → (2nd𝑈):𝑈𝐴)
22 nfv 1912 . . . . . . . . 9 𝑥𝜑
23 nfiu1 5032 . . . . . . . . . . 11 𝑥 𝑥𝑋 ({𝑥} × 𝐶)
249, 23nfcxfr 2901 . . . . . . . . . 10 𝑥𝑈
2524nfcri 2895 . . . . . . . . 9 𝑥 𝑢𝑈
2622, 25nfan 1897 . . . . . . . 8 𝑥(𝜑𝑢𝑈)
2724nfcri 2895 . . . . . . . 8 𝑥 𝑣𝑈
2826, 27nfan 1897 . . . . . . 7 𝑥((𝜑𝑢𝑈) ∧ 𝑣𝑈)
29 nfcv 2903 . . . . . . . . . 10 𝑥2nd
3029, 24nfres 6002 . . . . . . . . 9 𝑥(2nd𝑈)
31 nfcv 2903 . . . . . . . . 9 𝑥𝑢
3230, 31nffv 6917 . . . . . . . 8 𝑥((2nd𝑈)‘𝑢)
33 nfcv 2903 . . . . . . . . 9 𝑥𝑣
3430, 33nffv 6917 . . . . . . . 8 𝑥((2nd𝑈)‘𝑣)
3532, 34nfeq 2917 . . . . . . 7 𝑥((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)
3628, 35nfan 1897 . . . . . 6 𝑥(((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣))
37 nfv 1912 . . . . . 6 𝑥 𝑢 = 𝑣
389eleq2i 2831 . . . . . . . 8 (𝑢𝑈𝑢 𝑥𝑋 ({𝑥} × 𝐶))
39 eliunxp 5851 . . . . . . . 8 (𝑢 𝑥𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)))
4038, 39sylbb 219 . . . . . . 7 (𝑢𝑈 → ∃𝑥𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)))
4140ad3antlr 731 . . . . . 6 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → ∃𝑥𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)))
429eleq2i 2831 . . . . . . . . . . . . 13 (𝑣𝑈𝑣 𝑥𝑋 ({𝑥} × 𝐶))
43 eliunxp 5851 . . . . . . . . . . . . 13 (𝑣 𝑥𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)))
4442, 43bitri 275 . . . . . . . . . . . 12 (𝑣𝑈 ↔ ∃𝑥𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)))
45 nfv 1912 . . . . . . . . . . . . 13 𝑦𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶))
46 nfv 1912 . . . . . . . . . . . . . . 15 𝑥 𝑣 = ⟨𝑦, 𝑑
47 nfv 1912 . . . . . . . . . . . . . . . 16 𝑥 𝑦𝑋
48 nfcsb1v 3933 . . . . . . . . . . . . . . . . 17 𝑥𝑦 / 𝑥𝐶
4948nfcri 2895 . . . . . . . . . . . . . . . 16 𝑥 𝑑𝑦 / 𝑥𝐶
5047, 49nfan 1897 . . . . . . . . . . . . . . 15 𝑥(𝑦𝑋𝑑𝑦 / 𝑥𝐶)
5146, 50nfan 1897 . . . . . . . . . . . . . 14 𝑥(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))
5251nfex 2323 . . . . . . . . . . . . 13 𝑥𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))
53 opeq1 4878 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ⟨𝑥, 𝑑⟩ = ⟨𝑦, 𝑑⟩)
5453eqeq2d 2746 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑣 = ⟨𝑥, 𝑑⟩ ↔ 𝑣 = ⟨𝑦, 𝑑⟩))
55 eleq1w 2822 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥𝑋𝑦𝑋))
56 csbeq1a 3922 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦𝐶 = 𝑦 / 𝑥𝐶)
5756eleq2d 2825 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑑𝐶𝑑𝑦 / 𝑥𝐶))
5855, 57anbi12d 632 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑥𝑋𝑑𝐶) ↔ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)))
5954, 58anbi12d 632 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)) ↔ (𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))))
6059exbidv 1919 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)) ↔ ∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))))
6145, 52, 60cbvexv1 2343 . . . . . . . . . . . 12 (∃𝑥𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)) ↔ ∃𝑦𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)))
6244, 61sylbb 219 . . . . . . . . . . 11 (𝑣𝑈 → ∃𝑦𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)))
6362ad5antlr 735 . . . . . . . . . 10 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → ∃𝑦𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)))
64 2ndresdju.1 . . . . . . . . . . . . . . . . 17 (𝜑Disj 𝑥𝑋 𝐶)
6564ad9antr 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𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑢𝑈)
7170fvresd 6927 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑢) = (2nd𝑢))
72 simp-6r 788 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑢 = ⟨𝑥, 𝑐⟩)
7372fveq2d 6911 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑢) = (2nd ‘⟨𝑥, 𝑐⟩))
74 vex 3482 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
75 vex 3482 . . . . . . . . . . . . . . . . . . . . 21 𝑐 ∈ V
7674, 75op2nd 8022 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘⟨𝑥, 𝑐⟩) = 𝑐
7773, 76eqtrdi 2791 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑢) = 𝑐)
7871, 77eqtrd 2775 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑢) = 𝑐)
79 simp-8r 792 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑣𝑈)
8079fvresd 6927 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑣) = (2nd𝑣))
81 simpllr 776 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑣 = ⟨𝑦, 𝑑⟩)
8281fveq2d 6911 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑣) = (2nd ‘⟨𝑦, 𝑑⟩))
83 vex 3482 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
84 vex 3482 . . . . . . . . . . . . . . . . . . . . 21 𝑑 ∈ V
8583, 84op2nd 8022 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘⟨𝑦, 𝑑⟩) = 𝑑
8682, 85eqtrdi 2791 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑣) = 𝑑)
8780, 86eqtrd 2775 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑣) = 𝑑)
8869, 78, 873eqtr3d 2783 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑐 = 𝑑)
89 simpr 484 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑑𝑦 / 𝑥𝐶)
9088, 89eqeltrd 2839 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑐𝑦 / 𝑥𝐶)
9148, 56disjif 32598 . . . . . . . . . . . . . . . 16 ((Disj 𝑥𝑋 𝐶 ∧ (𝑥𝑋𝑦𝑋) ∧ (𝑐𝐶𝑐𝑦 / 𝑥𝐶)) → 𝑥 = 𝑦)
9265, 66, 67, 68, 90, 91syl122anc 1378 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑥 = 𝑦)
9392, 88opeq12d 4886 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ⟨𝑥, 𝑐⟩ = ⟨𝑦, 𝑑⟩)
9493, 72, 813eqtr4d 2785 . . . . . . . . . . . . 13 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑢 = 𝑣)
9594anasss 466 . . . . . . . . . . . 12 (((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)) → 𝑢 = 𝑣)
9695expl 457 . . . . . . . . . . 11 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → ((𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)) → 𝑢 = 𝑣))
9796exlimdvv 1932 . . . . . . . . . 10 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → (∃𝑦𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)) → 𝑢 = 𝑣))
9863, 97mpd 15 . . . . . . . . 9 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → 𝑢 = 𝑣)
9998anasss 466 . . . . . . . 8 ((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ (𝑥𝑋𝑐𝐶)) → 𝑢 = 𝑣)
10099expl 457 . . . . . . 7 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → ((𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)) → 𝑢 = 𝑣))
101100exlimdv 1931 . . . . . 6 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → (∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)) → 𝑢 = 𝑣))
10236, 37, 41, 101exlimimdd 2217 . . . . 5 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → 𝑢 = 𝑣)
103102ex 412 . . . 4 (((𝜑𝑢𝑈) ∧ 𝑣𝑈) → (((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣) → 𝑢 = 𝑣))
104103anasss 466 . . 3 ((𝜑 ∧ (𝑢𝑈𝑣𝑈)) → (((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣) → 𝑢 = 𝑣))
105104ralrimivva 3200 . 2 (𝜑 → ∀𝑢𝑈𝑣𝑈 (((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣) → 𝑢 = 𝑣))
106 dff13 7275 . 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 395   = wceq 1537  wex 1776  wcel 2106  wral 3059  Vcvv 3478  csb 3908  wss 3963  {csn 4631  cop 4637   ciun 4996  Disj wdisj 5115   × cxp 5687  cres 5691   Fn wfn 6558  wf 6559  1-1wf1 6560  ontowfo 6561  cfv 6563  2nd c2nd 8012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-disj 5116  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-fv 6571  df-2nd 8014
This theorem is referenced by:  2ndresdjuf1o  32667  gsumpart  33043
  Copyright terms: Public domain W3C validator