Step | Hyp | Ref
| Expression |
1 | | fo2nd 7707 |
. . . . 5
⊢
2nd :V–onto→V |
2 | | fofn 6571 |
. . . . 5
⊢
(2nd :V–onto→V → 2nd Fn V) |
3 | 1, 2 | mp1i 13 |
. . . 4
⊢ (𝜑 → 2nd Fn
V) |
4 | | ssv 3912 |
. . . . 5
⊢ 𝑈 ⊆ V |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑈 ⊆ V) |
6 | 3, 5 | fnssresd 6447 |
. . 3
⊢ (𝜑 → (2nd ↾
𝑈) Fn 𝑈) |
7 | | simpr 489 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝑈) |
8 | 7 | fvresd 6671 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢)) |
9 | | 2ndresdju.u |
. . . . . . . 8
⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) |
10 | | djussxp2 30493 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × ∪
𝑥 ∈ 𝑋 𝐶) |
11 | | 2ndresdju.2 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴) |
12 | 11 | xpeq2d 5547 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 × ∪
𝑥 ∈ 𝑋 𝐶) = (𝑋 × 𝐴)) |
13 | 10, 12 | sseqtrid 3940 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴)) |
14 | 9, 13 | eqsstrid 3936 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ⊆ (𝑋 × 𝐴)) |
15 | 14 | sselda 3888 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ (𝑋 × 𝐴)) |
16 | | xp2nd 7719 |
. . . . . 6
⊢ (𝑢 ∈ (𝑋 × 𝐴) → (2nd ‘𝑢) ∈ 𝐴) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (2nd ‘𝑢) ∈ 𝐴) |
18 | 8, 17 | eqeltrd 2851 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴) |
19 | 18 | ralrimiva 3111 |
. . 3
⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴) |
20 | | ffnfv 6866 |
. . 3
⊢
((2nd ↾ 𝑈):𝑈⟶𝐴 ↔ ((2nd ↾ 𝑈) Fn 𝑈 ∧ ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴)) |
21 | 6, 19, 20 | sylanbrc 587 |
. 2
⊢ (𝜑 → (2nd ↾
𝑈):𝑈⟶𝐴) |
22 | | nfv 1916 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝜑 |
23 | | nfiu1 4910 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) |
24 | 9, 23 | nfcxfr 2915 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑈 |
25 | 24 | nfcri 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑢 ∈ 𝑈 |
26 | 22, 25 | nfan 1901 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ 𝑈) |
27 | 24 | nfcri 2904 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑣 ∈ 𝑈 |
28 | 26, 27 | nfan 1901 |
. . . . . . 7
⊢
Ⅎ𝑥((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) |
29 | | nfcv 2917 |
. . . . . . . . . 10
⊢
Ⅎ𝑥2nd |
30 | 29, 24 | nfres 5818 |
. . . . . . . . 9
⊢
Ⅎ𝑥(2nd ↾ 𝑈) |
31 | | nfcv 2917 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑢 |
32 | 30, 31 | nffv 6661 |
. . . . . . . 8
⊢
Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢) |
33 | | nfcv 2917 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑣 |
34 | 30, 33 | nffv 6661 |
. . . . . . . 8
⊢
Ⅎ𝑥((2nd ↾ 𝑈)‘𝑣) |
35 | 32, 34 | nfeq 2930 |
. . . . . . 7
⊢
Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) |
36 | 28, 35 | nfan 1901 |
. . . . . 6
⊢
Ⅎ𝑥(((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) |
37 | | nfv 1916 |
. . . . . 6
⊢
Ⅎ𝑥 𝑢 = 𝑣 |
38 | 9 | eleq2i 2842 |
. . . . . . . 8
⊢ (𝑢 ∈ 𝑈 ↔ 𝑢 ∈ ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) |
39 | | eliunxp 5670 |
. . . . . . . 8
⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑐(𝑢 = 〈𝑥, 𝑐〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶))) |
40 | 38, 39 | sylbb 222 |
. . . . . . 7
⊢ (𝑢 ∈ 𝑈 → ∃𝑥∃𝑐(𝑢 = 〈𝑥, 𝑐〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶))) |
41 | 40 | ad3antlr 731 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ∃𝑥∃𝑐(𝑢 = 〈𝑥, 𝑐〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶))) |
42 | 9 | eleq2i 2842 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ 𝑈 ↔ 𝑣 ∈ ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) |
43 | | eliunxp 5670 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑑(𝑣 = 〈𝑥, 𝑑〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶))) |
44 | 42, 43 | bitri 278 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ 𝑈 ↔ ∃𝑥∃𝑑(𝑣 = 〈𝑥, 𝑑〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶))) |
45 | | nfv 1916 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦∃𝑑(𝑣 = 〈𝑥, 𝑑〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) |
46 | | nfv 1916 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥 𝑣 = 〈𝑦, 𝑑〉 |
47 | | nfv 1916 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝑦 ∈ 𝑋 |
48 | | nfcsb1v 3825 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶 |
49 | 48 | nfcri 2904 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶 |
50 | 47, 49 | nfan 1901 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) |
51 | 46, 50 | nfan 1901 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
52 | 51 | nfex 2333 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥∃𝑑(𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
53 | | opeq1 4754 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑑〉 = 〈𝑦, 𝑑〉) |
54 | 53 | eqeq2d 2770 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑣 = 〈𝑥, 𝑑〉 ↔ 𝑣 = 〈𝑦, 𝑑〉)) |
55 | | eleq1w 2833 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋)) |
56 | | csbeq1a 3815 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶) |
57 | 56 | eleq2d 2836 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑑 ∈ 𝐶 ↔ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
58 | 55, 57 | anbi12d 634 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶) ↔ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))) |
59 | 54, 58 | anbi12d 634 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝑣 = 〈𝑥, 𝑑〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ (𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))) |
60 | 59 | exbidv 1923 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (∃𝑑(𝑣 = 〈𝑥, 𝑑〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ ∃𝑑(𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))) |
61 | 45, 52, 60 | cbvexv1 2352 |
. . . . . . . . . . . 12
⊢
(∃𝑥∃𝑑(𝑣 = 〈𝑥, 𝑑〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ ∃𝑦∃𝑑(𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))) |
62 | 44, 61 | sylbb 222 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝑈 → ∃𝑦∃𝑑(𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))) |
63 | 62 | ad5antlr 735 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → ∃𝑦∃𝑑(𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))) |
64 | | 2ndresdju.1 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶) |
65 | 64 | ad9antr 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 ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 ∈ 𝑈) |
71 | 70 | fvresd 6671 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢)) |
72 | | simp-6r 788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = 〈𝑥, 𝑐〉) |
73 | 72 | fveq2d 6655 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = (2nd
‘〈𝑥, 𝑐〉)) |
74 | | vex 3411 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑥 ∈ V |
75 | | vex 3411 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑐 ∈ V |
76 | 74, 75 | op2nd 7695 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘〈𝑥, 𝑐〉) = 𝑐 |
77 | 73, 76 | eqtrdi 2810 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = 𝑐) |
78 | 71, 77 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = 𝑐) |
79 | | simp-8r 792 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 ∈ 𝑈) |
80 | 79 | fvresd 6671 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = (2nd ‘𝑣)) |
81 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 = 〈𝑦, 𝑑〉) |
82 | 81 | fveq2d 6655 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = (2nd
‘〈𝑦, 𝑑〉)) |
83 | | vex 3411 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑦 ∈ V |
84 | | vex 3411 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑑 ∈ V |
85 | 83, 84 | op2nd 7695 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘〈𝑦, 𝑑〉) = 𝑑 |
86 | 82, 85 | eqtrdi 2810 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = 𝑑) |
87 | 80, 86 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = 𝑑) |
88 | 69, 78, 87 | 3eqtr3d 2802 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 = 𝑑) |
89 | | simpr 489 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) |
90 | 88, 89 | eqeltrd 2851 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶) |
91 | 48, 56 | disjif 30424 |
. . . . . . . . . . . . . . . 16
⊢
((Disj 𝑥
∈ 𝑋 𝐶 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑥 = 𝑦) |
92 | 65, 66, 67, 68, 90, 91 | syl122anc 1377 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑥 = 𝑦) |
93 | 92, 88 | opeq12d 4764 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 〈𝑥, 𝑐〉 = 〈𝑦, 𝑑〉) |
94 | 93, 72, 81 | 3eqtr4d 2804 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = 𝑣) |
95 | 94 | anasss 471 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣) |
96 | 95 | expl 462 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → ((𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣)) |
97 | 96 | exlimdvv 1936 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → (∃𝑦∃𝑑(𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣)) |
98 | 63, 97 | mpd 15 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → 𝑢 = 𝑣) |
99 | 98 | anasss 471 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣) |
100 | 99 | expl 462 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ((𝑢 = 〈𝑥, 𝑐〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣)) |
101 | 100 | exlimdv 1935 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → (∃𝑐(𝑢 = 〈𝑥, 𝑐〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣)) |
102 | 36, 37, 41, 101 | exlimimdd 2218 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → 𝑢 = 𝑣) |
103 | 102 | ex 417 |
. . . 4
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣)) |
104 | 103 | anasss 471 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣)) |
105 | 104 | ralrimivva 3118 |
. 2
⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣)) |
106 | | dff13 6998 |
. 2
⊢
((2nd ↾ 𝑈):𝑈–1-1→𝐴 ↔ ((2nd ↾ 𝑈):𝑈⟶𝐴 ∧ ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))) |
107 | 21, 105, 106 | sylanbrc 587 |
1
⊢ (𝜑 → (2nd ↾
𝑈):𝑈–1-1→𝐴) |