| Step | Hyp | Ref
| Expression |
| 1 | | fo2nd 8035 |
. . . . 5
⊢
2nd :V–onto→V |
| 2 | | fofn 6822 |
. . . . 5
⊢
(2nd :V–onto→V → 2nd Fn V) |
| 3 | 1, 2 | mp1i 13 |
. . . 4
⊢ (𝜑 → 2nd Fn
V) |
| 4 | | ssv 4008 |
. . . . 5
⊢ 𝑈 ⊆ V |
| 5 | 4 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑈 ⊆ V) |
| 6 | 3, 5 | fnssresd 6692 |
. . 3
⊢ (𝜑 → (2nd ↾
𝑈) Fn 𝑈) |
| 7 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝑈) |
| 8 | 7 | fvresd 6926 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢)) |
| 9 | | 2ndresdju.u |
. . . . . . . 8
⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) |
| 10 | | djussxp2 32658 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × ∪
𝑥 ∈ 𝑋 𝐶) |
| 11 | | 2ndresdju.2 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴) |
| 12 | 11 | xpeq2d 5715 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 × ∪
𝑥 ∈ 𝑋 𝐶) = (𝑋 × 𝐴)) |
| 13 | 10, 12 | sseqtrid 4026 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴)) |
| 14 | 9, 13 | eqsstrid 4022 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ⊆ (𝑋 × 𝐴)) |
| 15 | 14 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ (𝑋 × 𝐴)) |
| 16 | | xp2nd 8047 |
. . . . . 6
⊢ (𝑢 ∈ (𝑋 × 𝐴) → (2nd ‘𝑢) ∈ 𝐴) |
| 17 | 15, 16 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (2nd ‘𝑢) ∈ 𝐴) |
| 18 | 8, 17 | eqeltrd 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴) |
| 19 | 18 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴) |
| 20 | | ffnfv 7139 |
. . 3
⊢
((2nd ↾ 𝑈):𝑈⟶𝐴 ↔ ((2nd ↾ 𝑈) Fn 𝑈 ∧ ∀𝑢 ∈ 𝑈 ((2nd ↾ 𝑈)‘𝑢) ∈ 𝐴)) |
| 21 | 6, 19, 20 | sylanbrc 583 |
. 2
⊢ (𝜑 → (2nd ↾
𝑈):𝑈⟶𝐴) |
| 22 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝜑 |
| 23 | | nfiu1 5027 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) |
| 24 | 9, 23 | nfcxfr 2903 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑈 |
| 25 | 24 | nfcri 2897 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑢 ∈ 𝑈 |
| 26 | 22, 25 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ 𝑈) |
| 27 | 24 | nfcri 2897 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑣 ∈ 𝑈 |
| 28 | 26, 27 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑥((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) |
| 29 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑥2nd |
| 30 | 29, 24 | nfres 5999 |
. . . . . . . . 9
⊢
Ⅎ𝑥(2nd ↾ 𝑈) |
| 31 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑢 |
| 32 | 30, 31 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢) |
| 33 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑣 |
| 34 | 30, 33 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑥((2nd ↾ 𝑈)‘𝑣) |
| 35 | 32, 34 | nfeq 2919 |
. . . . . . 7
⊢
Ⅎ𝑥((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) |
| 36 | 28, 35 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑥(((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) |
| 37 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑥 𝑢 = 𝑣 |
| 38 | 9 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑢 ∈ 𝑈 ↔ 𝑢 ∈ ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) |
| 39 | | eliunxp 5848 |
. . . . . . . 8
⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑐(𝑢 = 〈𝑥, 𝑐〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶))) |
| 40 | 38, 39 | sylbb 219 |
. . . . . . 7
⊢ (𝑢 ∈ 𝑈 → ∃𝑥∃𝑐(𝑢 = 〈𝑥, 𝑐〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶))) |
| 41 | 40 | ad3antlr 731 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ∃𝑥∃𝑐(𝑢 = 〈𝑥, 𝑐〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶))) |
| 42 | 9 | eleq2i 2833 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ 𝑈 ↔ 𝑣 ∈ ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) |
| 43 | | eliunxp 5848 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥∃𝑑(𝑣 = 〈𝑥, 𝑑〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶))) |
| 44 | 42, 43 | bitri 275 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ 𝑈 ↔ ∃𝑥∃𝑑(𝑣 = 〈𝑥, 𝑑〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶))) |
| 45 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦∃𝑑(𝑣 = 〈𝑥, 𝑑〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) |
| 46 | | nfv 1914 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥 𝑣 = 〈𝑦, 𝑑〉 |
| 47 | | nfv 1914 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝑦 ∈ 𝑋 |
| 48 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶 |
| 49 | 48 | nfcri 2897 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶 |
| 50 | 47, 49 | nfan 1899 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) |
| 51 | 46, 50 | nfan 1899 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
| 52 | 51 | nfex 2324 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥∃𝑑(𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
| 53 | | opeq1 4873 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑑〉 = 〈𝑦, 𝑑〉) |
| 54 | 53 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑣 = 〈𝑥, 𝑑〉 ↔ 𝑣 = 〈𝑦, 𝑑〉)) |
| 55 | | eleq1w 2824 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋)) |
| 56 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶) |
| 57 | 56 | eleq2d 2827 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑑 ∈ 𝐶 ↔ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
| 58 | 55, 57 | anbi12d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶) ↔ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))) |
| 59 | 54, 58 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝑣 = 〈𝑥, 𝑑〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ (𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))) |
| 60 | 59 | exbidv 1921 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (∃𝑑(𝑣 = 〈𝑥, 𝑑〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ ∃𝑑(𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)))) |
| 61 | 45, 52, 60 | cbvexv1 2344 |
. . . . . . . . . . . 12
⊢
(∃𝑥∃𝑑(𝑣 = 〈𝑥, 𝑑〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑑 ∈ 𝐶)) ↔ ∃𝑦∃𝑑(𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶))) |
| 62 | 44, 61 | sylbb 219 |
. . . . . . . . . . 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 6926 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = (2nd ‘𝑢)) |
| 72 | | simp-6r 788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = 〈𝑥, 𝑐〉) |
| 73 | 72 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = (2nd
‘〈𝑥, 𝑐〉)) |
| 74 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑥 ∈ V |
| 75 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑐 ∈ V |
| 76 | 74, 75 | op2nd 8023 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘〈𝑥, 𝑐〉) = 𝑐 |
| 77 | 73, 76 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑢) = 𝑐) |
| 78 | 71, 77 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑢) = 𝑐) |
| 79 | | simp-8r 792 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 ∈ 𝑈) |
| 80 | 79 | fvresd 6926 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = (2nd ‘𝑣)) |
| 81 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑣 = 〈𝑦, 𝑑〉) |
| 82 | 81 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = (2nd
‘〈𝑦, 𝑑〉)) |
| 83 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑦 ∈ V |
| 84 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑑 ∈ V |
| 85 | 83, 84 | op2nd 8023 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘〈𝑦, 𝑑〉) = 𝑑 |
| 86 | 82, 85 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → (2nd ‘𝑣) = 𝑑) |
| 87 | 80, 86 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → ((2nd ↾ 𝑈)‘𝑣) = 𝑑) |
| 88 | 69, 78, 87 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 = 𝑑) |
| 89 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) |
| 90 | 88, 89 | eqeltrd 2841 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶) |
| 91 | 48, 56 | disjif 32591 |
. . . . . . . . . . . . . . . 16
⊢
((Disj 𝑥
∈ 𝑋 𝐶 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑥 = 𝑦) |
| 92 | 65, 66, 67, 68, 90, 91 | syl122anc 1381 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑥 = 𝑦) |
| 93 | 92, 88 | opeq12d 4881 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 〈𝑥, 𝑐〉 = 〈𝑦, 𝑑〉) |
| 94 | 93, 72, 81 | 3eqtr4d 2787 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ 𝑦 ∈ 𝑋) ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶) → 𝑢 = 𝑣) |
| 95 | 94 | anasss 466 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) ∧ 𝑣 = 〈𝑦, 𝑑〉) ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣) |
| 96 | 95 | expl 457 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → ((𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣)) |
| 97 | 96 | exlimdvv 1934 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → (∃𝑦∃𝑑(𝑣 = 〈𝑦, 𝑑〉 ∧ (𝑦 ∈ 𝑋 ∧ 𝑑 ∈ ⦋𝑦 / 𝑥⦌𝐶)) → 𝑢 = 𝑣)) |
| 98 | 63, 97 | mpd 15 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ 𝐶) → 𝑢 = 𝑣) |
| 99 | 98 | anasss 466 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) ∧ 𝑢 = 〈𝑥, 𝑐〉) ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣) |
| 100 | 99 | expl 457 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → ((𝑢 = 〈𝑥, 𝑐〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣)) |
| 101 | 100 | exlimdv 1933 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → (∃𝑐(𝑢 = 〈𝑥, 𝑐〉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑐 ∈ 𝐶)) → 𝑢 = 𝑣)) |
| 102 | 36, 37, 41, 101 | exlimimdd 2219 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ ((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣)) → 𝑢 = 𝑣) |
| 103 | 102 | ex 412 |
. . . 4
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣)) |
| 104 | 103 | anasss 466 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣)) |
| 105 | 104 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣)) |
| 106 | | dff13 7275 |
. 2
⊢
((2nd ↾ 𝑈):𝑈–1-1→𝐴 ↔ ((2nd ↾ 𝑈):𝑈⟶𝐴 ∧ ∀𝑢 ∈ 𝑈 ∀𝑣 ∈ 𝑈 (((2nd ↾ 𝑈)‘𝑢) = ((2nd ↾ 𝑈)‘𝑣) → 𝑢 = 𝑣))) |
| 107 | 21, 105, 106 | sylanbrc 583 |
1
⊢ (𝜑 → (2nd ↾
𝑈):𝑈–1-1→𝐴) |