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 32659
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 8035 . . . . 5 2nd :V–onto→V
2 fofn 6822 . . . . 5 (2nd :V–onto→V → 2nd Fn V)
31, 2mp1i 13 . . . 4 (𝜑 → 2nd Fn V)
4 ssv 4008 . . . . 5 𝑈 ⊆ V
54a1i 11 . . . 4 (𝜑𝑈 ⊆ V)
63, 5fnssresd 6692 . . 3 (𝜑 → (2nd𝑈) Fn 𝑈)
7 simpr 484 . . . . . 6 ((𝜑𝑢𝑈) → 𝑢𝑈)
87fvresd 6926 . . . . 5 ((𝜑𝑢𝑈) → ((2nd𝑈)‘𝑢) = (2nd𝑢))
9 2ndresdju.u . . . . . . . 8 𝑈 = 𝑥𝑋 ({𝑥} × 𝐶)
10 djussxp2 32658 . . . . . . . . 9 𝑥𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝑥𝑋 𝐶)
11 2ndresdju.2 . . . . . . . . . 10 (𝜑 𝑥𝑋 𝐶 = 𝐴)
1211xpeq2d 5715 . . . . . . . . 9 (𝜑 → (𝑋 × 𝑥𝑋 𝐶) = (𝑋 × 𝐴))
1310, 12sseqtrid 4026 . . . . . . . 8 (𝜑 𝑥𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴))
149, 13eqsstrid 4022 . . . . . . 7 (𝜑𝑈 ⊆ (𝑋 × 𝐴))
1514sselda 3983 . . . . . 6 ((𝜑𝑢𝑈) → 𝑢 ∈ (𝑋 × 𝐴))
16 xp2nd 8047 . . . . . 6 (𝑢 ∈ (𝑋 × 𝐴) → (2nd𝑢) ∈ 𝐴)
1715, 16syl 17 . . . . 5 ((𝜑𝑢𝑈) → (2nd𝑢) ∈ 𝐴)
188, 17eqeltrd 2841 . . . 4 ((𝜑𝑢𝑈) → ((2nd𝑈)‘𝑢) ∈ 𝐴)
1918ralrimiva 3146 . . 3 (𝜑 → ∀𝑢𝑈 ((2nd𝑈)‘𝑢) ∈ 𝐴)
20 ffnfv 7139 . . 3 ((2nd𝑈):𝑈𝐴 ↔ ((2nd𝑈) Fn 𝑈 ∧ ∀𝑢𝑈 ((2nd𝑈)‘𝑢) ∈ 𝐴))
216, 19, 20sylanbrc 583 . 2 (𝜑 → (2nd𝑈):𝑈𝐴)
22 nfv 1914 . . . . . . . . 9 𝑥𝜑
23 nfiu1 5027 . . . . . . . . . . 11 𝑥 𝑥𝑋 ({𝑥} × 𝐶)
249, 23nfcxfr 2903 . . . . . . . . . 10 𝑥𝑈
2524nfcri 2897 . . . . . . . . 9 𝑥 𝑢𝑈
2622, 25nfan 1899 . . . . . . . 8 𝑥(𝜑𝑢𝑈)
2724nfcri 2897 . . . . . . . 8 𝑥 𝑣𝑈
2826, 27nfan 1899 . . . . . . 7 𝑥((𝜑𝑢𝑈) ∧ 𝑣𝑈)
29 nfcv 2905 . . . . . . . . . 10 𝑥2nd
3029, 24nfres 5999 . . . . . . . . 9 𝑥(2nd𝑈)
31 nfcv 2905 . . . . . . . . 9 𝑥𝑢
3230, 31nffv 6916 . . . . . . . 8 𝑥((2nd𝑈)‘𝑢)
33 nfcv 2905 . . . . . . . . 9 𝑥𝑣
3430, 33nffv 6916 . . . . . . . 8 𝑥((2nd𝑈)‘𝑣)
3532, 34nfeq 2919 . . . . . . 7 𝑥((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)
3628, 35nfan 1899 . . . . . 6 𝑥(((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣))
37 nfv 1914 . . . . . 6 𝑥 𝑢 = 𝑣
389eleq2i 2833 . . . . . . . 8 (𝑢𝑈𝑢 𝑥𝑋 ({𝑥} × 𝐶))
39 eliunxp 5848 . . . . . . . 8 (𝑢 𝑥𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)))
4038, 39sylbb 219 . . . . . . 7 (𝑢𝑈 → ∃𝑥𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)))
4140ad3antlr 731 . . . . . 6 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → ∃𝑥𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)))
429eleq2i 2833 . . . . . . . . . . . . 13 (𝑣𝑈𝑣 𝑥𝑋 ({𝑥} × 𝐶))
43 eliunxp 5848 . . . . . . . . . . . . 13 (𝑣 𝑥𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)))
4442, 43bitri 275 . . . . . . . . . . . 12 (𝑣𝑈 ↔ ∃𝑥𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)))
45 nfv 1914 . . . . . . . . . . . . 13 𝑦𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶))
46 nfv 1914 . . . . . . . . . . . . . . 15 𝑥 𝑣 = ⟨𝑦, 𝑑
47 nfv 1914 . . . . . . . . . . . . . . . 16 𝑥 𝑦𝑋
48 nfcsb1v 3923 . . . . . . . . . . . . . . . . 17 𝑥𝑦 / 𝑥𝐶
4948nfcri 2897 . . . . . . . . . . . . . . . 16 𝑥 𝑑𝑦 / 𝑥𝐶
5047, 49nfan 1899 . . . . . . . . . . . . . . 15 𝑥(𝑦𝑋𝑑𝑦 / 𝑥𝐶)
5146, 50nfan 1899 . . . . . . . . . . . . . 14 𝑥(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))
5251nfex 2324 . . . . . . . . . . . . 13 𝑥𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))
53 opeq1 4873 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ⟨𝑥, 𝑑⟩ = ⟨𝑦, 𝑑⟩)
5453eqeq2d 2748 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑣 = ⟨𝑥, 𝑑⟩ ↔ 𝑣 = ⟨𝑦, 𝑑⟩))
55 eleq1w 2824 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥𝑋𝑦𝑋))
56 csbeq1a 3913 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦𝐶 = 𝑦 / 𝑥𝐶)
5756eleq2d 2827 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑑𝐶𝑑𝑦 / 𝑥𝐶))
5855, 57anbi12d 632 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑥𝑋𝑑𝐶) ↔ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)))
5954, 58anbi12d 632 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)) ↔ (𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))))
6059exbidv 1921 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)) ↔ ∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))))
6145, 52, 60cbvexv1 2344 . . . . . . . . . . . 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 6926 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑢) = (2nd𝑢))
72 simp-6r 788 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑢 = ⟨𝑥, 𝑐⟩)
7372fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑢) = (2nd ‘⟨𝑥, 𝑐⟩))
74 vex 3484 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
75 vex 3484 . . . . . . . . . . . . . . . . . . . . 21 𝑐 ∈ V
7674, 75op2nd 8023 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘⟨𝑥, 𝑐⟩) = 𝑐
7773, 76eqtrdi 2793 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑢) = 𝑐)
7871, 77eqtrd 2777 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑢) = 𝑐)
79 simp-8r 792 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑣𝑈)
8079fvresd 6926 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑣) = (2nd𝑣))
81 simpllr 776 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑣 = ⟨𝑦, 𝑑⟩)
8281fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑣) = (2nd ‘⟨𝑦, 𝑑⟩))
83 vex 3484 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
84 vex 3484 . . . . . . . . . . . . . . . . . . . . 21 𝑑 ∈ V
8583, 84op2nd 8023 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘⟨𝑦, 𝑑⟩) = 𝑑
8682, 85eqtrdi 2793 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑣) = 𝑑)
8780, 86eqtrd 2777 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑣) = 𝑑)
8869, 78, 873eqtr3d 2785 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑐 = 𝑑)
89 simpr 484 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑑𝑦 / 𝑥𝐶)
9088, 89eqeltrd 2841 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑐𝑦 / 𝑥𝐶)
9148, 56disjif 32591 . . . . . . . . . . . . . . . 16 ((Disj 𝑥𝑋 𝐶 ∧ (𝑥𝑋𝑦𝑋) ∧ (𝑐𝐶𝑐𝑦 / 𝑥𝐶)) → 𝑥 = 𝑦)
9265, 66, 67, 68, 90, 91syl122anc 1381 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑥 = 𝑦)
9392, 88opeq12d 4881 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ⟨𝑥, 𝑐⟩ = ⟨𝑦, 𝑑⟩)
9493, 72, 813eqtr4d 2787 . . . . . . . . . . . . 13 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑢 = 𝑣)
9594anasss 466 . . . . . . . . . . . 12 (((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)) → 𝑢 = 𝑣)
9695expl 457 . . . . . . . . . . 11 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → ((𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)) → 𝑢 = 𝑣))
9796exlimdvv 1934 . . . . . . . . . 10 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → (∃𝑦𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)) → 𝑢 = 𝑣))
9863, 97mpd 15 . . . . . . . . 9 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → 𝑢 = 𝑣)
9998anasss 466 . . . . . . . 8 ((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ (𝑥𝑋𝑐𝐶)) → 𝑢 = 𝑣)
10099expl 457 . . . . . . 7 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → ((𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)) → 𝑢 = 𝑣))
101100exlimdv 1933 . . . . . 6 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → (∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)) → 𝑢 = 𝑣))
10236, 37, 41, 101exlimimdd 2219 . . . . 5 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → 𝑢 = 𝑣)
103102ex 412 . . . 4 (((𝜑𝑢𝑈) ∧ 𝑣𝑈) → (((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣) → 𝑢 = 𝑣))
104103anasss 466 . . 3 ((𝜑 ∧ (𝑢𝑈𝑣𝑈)) → (((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣) → 𝑢 = 𝑣))
105104ralrimivva 3202 . 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 1540  wex 1779  wcel 2108  wral 3061  Vcvv 3480  csb 3899  wss 3951  {csn 4626  cop 4632   ciun 4991  Disj wdisj 5110   × cxp 5683  cres 5687   Fn wfn 6556  wf 6557  1-1wf1 6558  ontowfo 6559  cfv 6561  2nd c2nd 8013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-fv 6569  df-2nd 8015
This theorem is referenced by:  2ndresdjuf1o  32660  gsumpart  33060
  Copyright terms: Public domain W3C validator