Metamath Proof Explorer


Theorem 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 ( 𝜑 → ( 2nd𝑈 ) : 𝑈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 2nd : V –onto→ V
7 fofn ( 2nd : V –onto→ V → 2nd Fn V )
8 6 7 mp1i ( 𝜑 → 2nd Fn V )
9 ssv 𝑈 ⊆ V
10 9 a1i ( 𝜑𝑈 ⊆ V )
11 8 10 fnssresd ( 𝜑 → ( 2nd𝑈 ) Fn 𝑈 )
12 simpr ( ( 𝜑𝑢𝑈 ) → 𝑢𝑈 )
13 12 fvresd ( ( 𝜑𝑢𝑈 ) → ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( 2nd𝑢 ) )
14 djussxp2 𝑥𝑋 ( { 𝑥 } × 𝐶 ) ⊆ ( 𝑋 × 𝑥𝑋 𝐶 )
15 5 xpeq2d ( 𝜑 → ( 𝑋 × 𝑥𝑋 𝐶 ) = ( 𝑋 × 𝐴 ) )
16 14 15 sseqtrid ( 𝜑 𝑥𝑋 ( { 𝑥 } × 𝐶 ) ⊆ ( 𝑋 × 𝐴 ) )
17 1 16 eqsstrid ( 𝜑𝑈 ⊆ ( 𝑋 × 𝐴 ) )
18 17 sselda ( ( 𝜑𝑢𝑈 ) → 𝑢 ∈ ( 𝑋 × 𝐴 ) )
19 xp2nd ( 𝑢 ∈ ( 𝑋 × 𝐴 ) → ( 2nd𝑢 ) ∈ 𝐴 )
20 18 19 syl ( ( 𝜑𝑢𝑈 ) → ( 2nd𝑢 ) ∈ 𝐴 )
21 13 20 eqeltrd ( ( 𝜑𝑢𝑈 ) → ( ( 2nd𝑈 ) ‘ 𝑢 ) ∈ 𝐴 )
22 21 ralrimiva ( 𝜑 → ∀ 𝑢𝑈 ( ( 2nd𝑈 ) ‘ 𝑢 ) ∈ 𝐴 )
23 ffnfv ( ( 2nd𝑈 ) : 𝑈𝐴 ↔ ( ( 2nd𝑈 ) Fn 𝑈 ∧ ∀ 𝑢𝑈 ( ( 2nd𝑈 ) ‘ 𝑢 ) ∈ 𝐴 ) )
24 11 22 23 sylanbrc ( 𝜑 → ( 2nd𝑈 ) : 𝑈𝐴 )
25 nfv 𝑥 𝜑
26 nfiu1 𝑥 𝑥𝑋 ( { 𝑥 } × 𝐶 )
27 1 26 nfcxfr 𝑥 𝑈
28 27 nfcri 𝑥 𝑢𝑈
29 25 28 nfan 𝑥 ( 𝜑𝑢𝑈 )
30 27 nfcri 𝑥 𝑣𝑈
31 29 30 nfan 𝑥 ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 )
32 nfcv 𝑥 2nd
33 32 27 nfres 𝑥 ( 2nd𝑈 )
34 nfcv 𝑥 𝑢
35 33 34 nffv 𝑥 ( ( 2nd𝑈 ) ‘ 𝑢 )
36 nfcv 𝑥 𝑣
37 33 36 nffv 𝑥 ( ( 2nd𝑈 ) ‘ 𝑣 )
38 35 37 nfeq 𝑥 ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 )
39 31 38 nfan 𝑥 ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) )
40 nfv 𝑥 𝑢 = 𝑣
41 1 eleq2i ( 𝑢𝑈𝑢 𝑥𝑋 ( { 𝑥 } × 𝐶 ) )
42 eliunxp ( 𝑢 𝑥𝑋 ( { 𝑥 } × 𝐶 ) ↔ ∃ 𝑥𝑐 ( 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ∧ ( 𝑥𝑋𝑐𝐶 ) ) )
43 41 42 sylbb ( 𝑢𝑈 → ∃ 𝑥𝑐 ( 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ∧ ( 𝑥𝑋𝑐𝐶 ) ) )
44 43 ad3antlr ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) → ∃ 𝑥𝑐 ( 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ∧ ( 𝑥𝑋𝑐𝐶 ) ) )
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 ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) → ∃ 𝑦𝑑 ( 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ∧ ( 𝑦𝑋𝑑 𝑦 / 𝑥 𝐶 ) ) )
67 4 ad9antr ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → Disj 𝑥𝑋 𝐶 )
68 simp-5r ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → 𝑥𝑋 )
69 simplr ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → 𝑦𝑋 )
70 simp-4r ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → 𝑐𝐶 )
71 simp-7r ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) )
72 simp-9r ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → 𝑢𝑈 )
73 72 fvresd ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( 2nd𝑢 ) )
74 simp-6r ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ )
75 74 fveq2d ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → ( 2nd𝑢 ) = ( 2nd ‘ ⟨ 𝑥 , 𝑐 ⟩ ) )
76 vex 𝑥 ∈ V
77 vex 𝑐 ∈ V
78 76 77 op2nd ( 2nd ‘ ⟨ 𝑥 , 𝑐 ⟩ ) = 𝑐
79 75 78 eqtrdi ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → ( 2nd𝑢 ) = 𝑐 )
80 73 79 eqtrd ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → ( ( 2nd𝑈 ) ‘ 𝑢 ) = 𝑐 )
81 simp-8r ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → 𝑣𝑈 )
82 81 fvresd ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → ( ( 2nd𝑈 ) ‘ 𝑣 ) = ( 2nd𝑣 ) )
83 simpllr ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ )
84 83 fveq2d ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → ( 2nd𝑣 ) = ( 2nd ‘ ⟨ 𝑦 , 𝑑 ⟩ ) )
85 vex 𝑦 ∈ V
86 vex 𝑑 ∈ V
87 85 86 op2nd ( 2nd ‘ ⟨ 𝑦 , 𝑑 ⟩ ) = 𝑑
88 84 87 eqtrdi ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → ( 2nd𝑣 ) = 𝑑 )
89 82 88 eqtrd ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → ( ( 2nd𝑈 ) ‘ 𝑣 ) = 𝑑 )
90 71 80 89 3eqtr3d ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → 𝑐 = 𝑑 )
91 simpr ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → 𝑑 𝑦 / 𝑥 𝐶 )
92 90 91 eqeltrd ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → 𝑐 𝑦 / 𝑥 𝐶 )
93 51 59 disjif ( ( Disj 𝑥𝑋 𝐶 ∧ ( 𝑥𝑋𝑦𝑋 ) ∧ ( 𝑐𝐶𝑐 𝑦 / 𝑥 𝐶 ) ) → 𝑥 = 𝑦 )
94 67 68 69 70 92 93 syl122anc ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → 𝑥 = 𝑦 )
95 94 90 opeq12d ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → ⟨ 𝑥 , 𝑐 ⟩ = ⟨ 𝑦 , 𝑑 ⟩ )
96 95 74 83 3eqtr4d ( ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ 𝑦𝑋 ) ∧ 𝑑 𝑦 / 𝑥 𝐶 ) → 𝑢 = 𝑣 )
97 96 anasss ( ( ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) ∧ 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ) ∧ ( 𝑦𝑋𝑑 𝑦 / 𝑥 𝐶 ) ) → 𝑢 = 𝑣 )
98 97 expl ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) → ( ( 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ∧ ( 𝑦𝑋𝑑 𝑦 / 𝑥 𝐶 ) ) → 𝑢 = 𝑣 ) )
99 98 exlimdvv ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) → ( ∃ 𝑦𝑑 ( 𝑣 = ⟨ 𝑦 , 𝑑 ⟩ ∧ ( 𝑦𝑋𝑑 𝑦 / 𝑥 𝐶 ) ) → 𝑢 = 𝑣 ) )
100 66 99 mpd ( ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ 𝑥𝑋 ) ∧ 𝑐𝐶 ) → 𝑢 = 𝑣 )
101 100 anasss ( ( ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) ∧ 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ) ∧ ( 𝑥𝑋𝑐𝐶 ) ) → 𝑢 = 𝑣 )
102 101 expl ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) → ( ( 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ∧ ( 𝑥𝑋𝑐𝐶 ) ) → 𝑢 = 𝑣 ) )
103 102 exlimdv ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) → ( ∃ 𝑐 ( 𝑢 = ⟨ 𝑥 , 𝑐 ⟩ ∧ ( 𝑥𝑋𝑐𝐶 ) ) → 𝑢 = 𝑣 ) )
104 39 40 44 103 exlimimdd ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) ) → 𝑢 = 𝑣 )
105 104 ex ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
106 105 anasss ( ( 𝜑 ∧ ( 𝑢𝑈𝑣𝑈 ) ) → ( ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
107 106 ralrimivva ( 𝜑 → ∀ 𝑢𝑈𝑣𝑈 ( ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
108 dff13 ( ( 2nd𝑈 ) : 𝑈1-1𝐴 ↔ ( ( 2nd𝑈 ) : 𝑈𝐴 ∧ ∀ 𝑢𝑈𝑣𝑈 ( ( ( 2nd𝑈 ) ‘ 𝑢 ) = ( ( 2nd𝑈 ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ) )
109 24 107 108 sylanbrc ( 𝜑 → ( 2nd𝑈 ) : 𝑈1-1𝐴 )