Step | Hyp | Ref
| Expression |
1 | | wunnat.1 |
. 2
⊢ (𝜑 → 𝑈 ∈ WUni) |
2 | | wunnat.2 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑈) |
3 | | wunnat.3 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑈) |
4 | 1, 2, 3 | wunfunc 17405 |
. . 3
⊢ (𝜑 → (𝐶 Func 𝐷) ∈ 𝑈) |
5 | 1, 4, 4 | wunxp 10338 |
. 2
⊢ (𝜑 → ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) ∈ 𝑈) |
6 | | homid 16919 |
. . . . . . 7
⊢ Hom =
Slot (Hom ‘ndx) |
7 | 6, 1, 3 | wunstr 16741 |
. . . . . 6
⊢ (𝜑 → (Hom ‘𝐷) ∈ 𝑈) |
8 | 1, 7 | wunrn 10343 |
. . . . 5
⊢ (𝜑 → ran (Hom ‘𝐷) ∈ 𝑈) |
9 | 1, 8 | wununi 10320 |
. . . 4
⊢ (𝜑 → ∪ ran (Hom ‘𝐷) ∈ 𝑈) |
10 | | baseid 16763 |
. . . . 5
⊢ Base =
Slot (Base‘ndx) |
11 | 10, 1, 2 | wunstr 16741 |
. . . 4
⊢ (𝜑 → (Base‘𝐶) ∈ 𝑈) |
12 | 1, 9, 11 | wunmap 10340 |
. . 3
⊢ (𝜑 → (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) ∈ 𝑈) |
13 | 1, 12 | wunpw 10321 |
. 2
⊢ (𝜑 → 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) ∈ 𝑈) |
14 | | fvex 6730 |
. . . . . 6
⊢
(1st ‘𝑓) ∈ V |
15 | | fvex 6730 |
. . . . . . . . 9
⊢
(1st ‘𝑔) ∈ V |
16 | | ovex 7246 |
. . . . . . . . . . . 12
⊢ (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) ∈ V |
17 | | ssrab2 3993 |
. . . . . . . . . . . . 13
⊢ {𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ⊆ X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) |
18 | | ovssunirn 7249 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ⊆ ∪ ran
(Hom ‘𝐷) |
19 | 18 | rgenw 3073 |
. . . . . . . . . . . . . . 15
⊢
∀𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ⊆ ∪ ran
(Hom ‘𝐷) |
20 | | ss2ixp 8591 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ⊆ ∪ ran
(Hom ‘𝐷) → X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ⊆ X𝑥 ∈ (Base‘𝐶)∪
ran (Hom ‘𝐷)) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ⊆ X𝑥 ∈ (Base‘𝐶)∪
ran (Hom ‘𝐷) |
22 | | fvex 6730 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝐶)
∈ V |
23 | | fvex 6730 |
. . . . . . . . . . . . . . . . 17
⊢ (Hom
‘𝐷) ∈
V |
24 | 23 | rnex 7690 |
. . . . . . . . . . . . . . . 16
⊢ ran (Hom
‘𝐷) ∈
V |
25 | 24 | uniex 7529 |
. . . . . . . . . . . . . . 15
⊢ ∪ ran (Hom ‘𝐷) ∈ V |
26 | 22, 25 | ixpconst 8588 |
. . . . . . . . . . . . . 14
⊢ X𝑥 ∈
(Base‘𝐶)∪ ran (Hom ‘𝐷) = (∪ ran (Hom
‘𝐷)
↑m (Base‘𝐶)) |
27 | 21, 26 | sseqtri 3937 |
. . . . . . . . . . . . 13
⊢ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ⊆ (∪ ran
(Hom ‘𝐷)
↑m (Base‘𝐶)) |
28 | 17, 27 | sstri 3910 |
. . . . . . . . . . . 12
⊢ {𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ⊆ (∪ ran
(Hom ‘𝐷)
↑m (Base‘𝐶)) |
29 | 16, 28 | elpwi2 5239 |
. . . . . . . . . . 11
⊢ {𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) |
30 | 29 | sbcth 3709 |
. . . . . . . . . 10
⊢
((1st ‘𝑔) ∈ V → [(1st
‘𝑔) / 𝑠]{𝑎 ∈ X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶))) |
31 | | sbcel1g 4328 |
. . . . . . . . . 10
⊢
((1st ‘𝑔) ∈ V → ([(1st
‘𝑔) / 𝑠]{𝑎 ∈ X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) ↔
⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)))) |
32 | 30, 31 | mpbid 235 |
. . . . . . . . 9
⊢
((1st ‘𝑔) ∈ V →
⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶))) |
33 | 15, 32 | ax-mp 5 |
. . . . . . . 8
⊢
⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) |
34 | 33 | sbcth 3709 |
. . . . . . 7
⊢
((1st ‘𝑓) ∈ V → [(1st
‘𝑓) / 𝑟]⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶))) |
35 | | sbcel1g 4328 |
. . . . . . 7
⊢
((1st ‘𝑓) ∈ V → ([(1st
‘𝑓) / 𝑟]⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) ↔
⦋(1st ‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)))) |
36 | 34, 35 | mpbid 235 |
. . . . . 6
⊢
((1st ‘𝑓) ∈ V →
⦋(1st ‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶))) |
37 | 14, 36 | ax-mp 5 |
. . . . 5
⊢
⦋(1st ‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) |
38 | 37 | rgen2w 3074 |
. . . 4
⊢
∀𝑓 ∈
(𝐶 Func 𝐷)∀𝑔 ∈ (𝐶 Func 𝐷)⦋(1st ‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) |
39 | | eqid 2737 |
. . . . . 6
⊢ (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷) |
40 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐶) =
(Base‘𝐶) |
41 | | eqid 2737 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
42 | | eqid 2737 |
. . . . . 6
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
43 | | eqid 2737 |
. . . . . 6
⊢
(comp‘𝐷) =
(comp‘𝐷) |
44 | 39, 40, 41, 42, 43 | natfval 17453 |
. . . . 5
⊢ (𝐶 Nat 𝐷) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))}) |
45 | 44 | fmpo 7838 |
. . . 4
⊢
(∀𝑓 ∈
(𝐶 Func 𝐷)∀𝑔 ∈ (𝐶 Func 𝐷)⦋(1st ‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) ↔ (𝐶 Nat 𝐷):((𝐶 Func 𝐷) × (𝐶 Func 𝐷))⟶𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶))) |
46 | 38, 45 | mpbi 233 |
. . 3
⊢ (𝐶 Nat 𝐷):((𝐶 Func 𝐷) × (𝐶 Func 𝐷))⟶𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) |
47 | 46 | a1i 11 |
. 2
⊢ (𝜑 → (𝐶 Nat 𝐷):((𝐶 Func 𝐷) × (𝐶 Func 𝐷))⟶𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶))) |
48 | 1, 5, 13, 47 | wunf 10341 |
1
⊢ (𝜑 → (𝐶 Nat 𝐷) ∈ 𝑈) |