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

Theorem 2ndresdju 30414
 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 7696 . . . . 5 2nd :V–onto→V
2 fofn 6571 . . . . 5 (2nd :V–onto→V → 2nd Fn V)
31, 2mp1i 13 . . . 4 (𝜑 → 2nd Fn V)
4 ssv 3942 . . . . 5 𝑈 ⊆ V
54a1i 11 . . . 4 (𝜑𝑈 ⊆ V)
63, 5fnssresd 6447 . . 3 (𝜑 → (2nd𝑈) Fn 𝑈)
7 simpr 488 . . . . . 6 ((𝜑𝑢𝑈) → 𝑢𝑈)
87fvresd 6669 . . . . 5 ((𝜑𝑢𝑈) → ((2nd𝑈)‘𝑢) = (2nd𝑢))
9 2ndresdju.u . . . . . . . 8 𝑈 = 𝑥𝑋 ({𝑥} × 𝐶)
10 djussxp2 30413 . . . . . . . . 9 𝑥𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝑥𝑋 𝐶)
11 2ndresdju.2 . . . . . . . . . 10 (𝜑 𝑥𝑋 𝐶 = 𝐴)
1211xpeq2d 5553 . . . . . . . . 9 (𝜑 → (𝑋 × 𝑥𝑋 𝐶) = (𝑋 × 𝐴))
1310, 12sseqtrid 3970 . . . . . . . 8 (𝜑 𝑥𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴))
149, 13eqsstrid 3966 . . . . . . 7 (𝜑𝑈 ⊆ (𝑋 × 𝐴))
1514sselda 3918 . . . . . 6 ((𝜑𝑢𝑈) → 𝑢 ∈ (𝑋 × 𝐴))
16 xp2nd 7708 . . . . . 6 (𝑢 ∈ (𝑋 × 𝐴) → (2nd𝑢) ∈ 𝐴)
1715, 16syl 17 . . . . 5 ((𝜑𝑢𝑈) → (2nd𝑢) ∈ 𝐴)
188, 17eqeltrd 2893 . . . 4 ((𝜑𝑢𝑈) → ((2nd𝑈)‘𝑢) ∈ 𝐴)
1918ralrimiva 3152 . . 3 (𝜑 → ∀𝑢𝑈 ((2nd𝑈)‘𝑢) ∈ 𝐴)
20 ffnfv 6863 . . 3 ((2nd𝑈):𝑈𝐴 ↔ ((2nd𝑈) Fn 𝑈 ∧ ∀𝑢𝑈 ((2nd𝑈)‘𝑢) ∈ 𝐴))
216, 19, 20sylanbrc 586 . 2 (𝜑 → (2nd𝑈):𝑈𝐴)
22 nfv 1915 . . . . . . . . 9 𝑥𝜑
23 nfiu1 4918 . . . . . . . . . . 11 𝑥 𝑥𝑋 ({𝑥} × 𝐶)
249, 23nfcxfr 2956 . . . . . . . . . 10 𝑥𝑈
2524nfcri 2946 . . . . . . . . 9 𝑥 𝑢𝑈
2622, 25nfan 1900 . . . . . . . 8 𝑥(𝜑𝑢𝑈)
2724nfcri 2946 . . . . . . . 8 𝑥 𝑣𝑈
2826, 27nfan 1900 . . . . . . 7 𝑥((𝜑𝑢𝑈) ∧ 𝑣𝑈)
29 nfcv 2958 . . . . . . . . . 10 𝑥2nd
3029, 24nfres 5824 . . . . . . . . 9 𝑥(2nd𝑈)
31 nfcv 2958 . . . . . . . . 9 𝑥𝑢
3230, 31nffv 6659 . . . . . . . 8 𝑥((2nd𝑈)‘𝑢)
33 nfcv 2958 . . . . . . . . 9 𝑥𝑣
3430, 33nffv 6659 . . . . . . . 8 𝑥((2nd𝑈)‘𝑣)
3532, 34nfeq 2971 . . . . . . 7 𝑥((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)
3628, 35nfan 1900 . . . . . 6 𝑥(((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣))
37 nfv 1915 . . . . . 6 𝑥 𝑢 = 𝑣
389eleq2i 2884 . . . . . . . 8 (𝑢𝑈𝑢 𝑥𝑋 ({𝑥} × 𝐶))
39 eliunxp 5676 . . . . . . . 8 (𝑢 𝑥𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)))
4038, 39sylbb 222 . . . . . . 7 (𝑢𝑈 → ∃𝑥𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)))
4140ad3antlr 730 . . . . . 6 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → ∃𝑥𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)))
429eleq2i 2884 . . . . . . . . . . . . 13 (𝑣𝑈𝑣 𝑥𝑋 ({𝑥} × 𝐶))
43 eliunxp 5676 . . . . . . . . . . . . 13 (𝑣 𝑥𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)))
4442, 43bitri 278 . . . . . . . . . . . 12 (𝑣𝑈 ↔ ∃𝑥𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)))
45 nfv 1915 . . . . . . . . . . . . 13 𝑦𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶))
46 nfv 1915 . . . . . . . . . . . . . . 15 𝑥 𝑣 = ⟨𝑦, 𝑑
47 nfv 1915 . . . . . . . . . . . . . . . 16 𝑥 𝑦𝑋
48 nfcsb1v 3855 . . . . . . . . . . . . . . . . 17 𝑥𝑦 / 𝑥𝐶
4948nfcri 2946 . . . . . . . . . . . . . . . 16 𝑥 𝑑𝑦 / 𝑥𝐶
5047, 49nfan 1900 . . . . . . . . . . . . . . 15 𝑥(𝑦𝑋𝑑𝑦 / 𝑥𝐶)
5146, 50nfan 1900 . . . . . . . . . . . . . 14 𝑥(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))
5251nfex 2335 . . . . . . . . . . . . 13 𝑥𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))
53 opeq1 4766 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ⟨𝑥, 𝑑⟩ = ⟨𝑦, 𝑑⟩)
5453eqeq2d 2812 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑣 = ⟨𝑥, 𝑑⟩ ↔ 𝑣 = ⟨𝑦, 𝑑⟩))
55 eleq1w 2875 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥𝑋𝑦𝑋))
56 csbeq1a 3845 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦𝐶 = 𝑦 / 𝑥𝐶)
5756eleq2d 2878 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑑𝐶𝑑𝑦 / 𝑥𝐶))
5855, 57anbi12d 633 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑥𝑋𝑑𝐶) ↔ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)))
5954, 58anbi12d 633 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)) ↔ (𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))))
6059exbidv 1922 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (∃𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)) ↔ ∃𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶))))
6145, 52, 60cbvexv1 2354 . . . . . . . . . . . 12 (∃𝑥𝑑(𝑣 = ⟨𝑥, 𝑑⟩ ∧ (𝑥𝑋𝑑𝐶)) ↔ ∃𝑦𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)))
6244, 61sylbb 222 . . . . . . . . . . 11 (𝑣𝑈 → ∃𝑦𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)))
6362ad5antlr 734 . . . . . . . . . 10 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → ∃𝑦𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)))
64 2ndresdju.1 . . . . . . . . . . . . . . . . 17 (𝜑Disj 𝑥𝑋 𝐶)
6564ad9antr 741 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → Disj 𝑥𝑋 𝐶)
66 simp-5r 785 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑥𝑋)
67 simplr 768 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑦𝑋)
68 simp-4r 783 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑐𝐶)
69 simp-7r 789 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣))
70 simp-9r 793 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑢𝑈)
7170fvresd 6669 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑢) = (2nd𝑢))
72 simp-6r 787 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑢 = ⟨𝑥, 𝑐⟩)
7372fveq2d 6653 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑢) = (2nd ‘⟨𝑥, 𝑐⟩))
74 vex 3447 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
75 vex 3447 . . . . . . . . . . . . . . . . . . . . 21 𝑐 ∈ V
7674, 75op2nd 7684 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘⟨𝑥, 𝑐⟩) = 𝑐
7773, 76eqtrdi 2852 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑢) = 𝑐)
7871, 77eqtrd 2836 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑢) = 𝑐)
79 simp-8r 791 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑣𝑈)
8079fvresd 6669 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑣) = (2nd𝑣))
81 simpllr 775 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑣 = ⟨𝑦, 𝑑⟩)
8281fveq2d 6653 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑣) = (2nd ‘⟨𝑦, 𝑑⟩))
83 vex 3447 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
84 vex 3447 . . . . . . . . . . . . . . . . . . . . 21 𝑑 ∈ V
8583, 84op2nd 7684 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘⟨𝑦, 𝑑⟩) = 𝑑
8682, 85eqtrdi 2852 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → (2nd𝑣) = 𝑑)
8780, 86eqtrd 2836 . . . . . . . . . . . . . . . . . 18 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ((2nd𝑈)‘𝑣) = 𝑑)
8869, 78, 873eqtr3d 2844 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑐 = 𝑑)
89 simpr 488 . . . . . . . . . . . . . . . . 17 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑑𝑦 / 𝑥𝐶)
9088, 89eqeltrd 2893 . . . . . . . . . . . . . . . 16 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑐𝑦 / 𝑥𝐶)
9148, 56disjif 30344 . . . . . . . . . . . . . . . 16 ((Disj 𝑥𝑋 𝐶 ∧ (𝑥𝑋𝑦𝑋) ∧ (𝑐𝐶𝑐𝑦 / 𝑥𝐶)) → 𝑥 = 𝑦)
9265, 66, 67, 68, 90, 91syl122anc 1376 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑥 = 𝑦)
9392, 88opeq12d 4776 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → ⟨𝑥, 𝑐⟩ = ⟨𝑦, 𝑑⟩)
9493, 72, 813eqtr4d 2846 . . . . . . . . . . . . 13 ((((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ 𝑦𝑋) ∧ 𝑑𝑦 / 𝑥𝐶) → 𝑢 = 𝑣)
9594anasss 470 . . . . . . . . . . . 12 (((((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) ∧ 𝑣 = ⟨𝑦, 𝑑⟩) ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)) → 𝑢 = 𝑣)
9695expl 461 . . . . . . . . . . 11 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → ((𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)) → 𝑢 = 𝑣))
9796exlimdvv 1935 . . . . . . . . . 10 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → (∃𝑦𝑑(𝑣 = ⟨𝑦, 𝑑⟩ ∧ (𝑦𝑋𝑑𝑦 / 𝑥𝐶)) → 𝑢 = 𝑣))
9863, 97mpd 15 . . . . . . . . 9 (((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ 𝑥𝑋) ∧ 𝑐𝐶) → 𝑢 = 𝑣)
9998anasss 470 . . . . . . . 8 ((((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) ∧ 𝑢 = ⟨𝑥, 𝑐⟩) ∧ (𝑥𝑋𝑐𝐶)) → 𝑢 = 𝑣)
10099expl 461 . . . . . . 7 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → ((𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)) → 𝑢 = 𝑣))
101100exlimdv 1934 . . . . . 6 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → (∃𝑐(𝑢 = ⟨𝑥, 𝑐⟩ ∧ (𝑥𝑋𝑐𝐶)) → 𝑢 = 𝑣))
10236, 37, 41, 101exlimimdd 2218 . . . . 5 ((((𝜑𝑢𝑈) ∧ 𝑣𝑈) ∧ ((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣)) → 𝑢 = 𝑣)
103102ex 416 . . . 4 (((𝜑𝑢𝑈) ∧ 𝑣𝑈) → (((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣) → 𝑢 = 𝑣))
104103anasss 470 . . 3 ((𝜑 ∧ (𝑢𝑈𝑣𝑈)) → (((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣) → 𝑢 = 𝑣))
105104ralrimivva 3159 . 2 (𝜑 → ∀𝑢𝑈𝑣𝑈 (((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣) → 𝑢 = 𝑣))
106 dff13 6995 . 2 ((2nd𝑈):𝑈1-1𝐴 ↔ ((2nd𝑈):𝑈𝐴 ∧ ∀𝑢𝑈𝑣𝑈 (((2nd𝑈)‘𝑢) = ((2nd𝑈)‘𝑣) → 𝑢 = 𝑣)))
10721, 105, 106sylanbrc 586 1 (𝜑 → (2nd𝑈):𝑈1-1𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2112  ∀wral 3109  Vcvv 3444  ⦋csb 3831   ⊆ wss 3884  {csn 4528  ⟨cop 4534  ∪ ciun 4884  Disj wdisj 4998   × cxp 5521   ↾ cres 5525   Fn wfn 6323  ⟶wf 6324  –1-1→wf1 6325  –onto→wfo 6326  ‘cfv 6328  2nd c2nd 7674 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-disj 4999  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-fv 6336  df-2nd 7676 This theorem is referenced by:  2ndresdjuf1o  30415  gsumpart  30743
 Copyright terms: Public domain W3C validator