| Step | Hyp | Ref
| Expression |
| 1 | | wunnat.1 |
. 2
⊢ (𝜑 → 𝑈 ∈ WUni) |
| 2 | | wunnat.2 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑈) |
| 3 | | wunnat.3 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑈) |
| 4 | 1, 2, 3 | wunfunc 17946 |
. . 3
⊢ (𝜑 → (𝐶 Func 𝐷) ∈ 𝑈) |
| 5 | 1, 4, 4 | wunxp 10764 |
. 2
⊢ (𝜑 → ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) ∈ 𝑈) |
| 6 | | homid 17456 |
. . . . . . 7
⊢ Hom =
Slot (Hom ‘ndx) |
| 7 | 6, 1, 3 | wunstr 17225 |
. . . . . 6
⊢ (𝜑 → (Hom ‘𝐷) ∈ 𝑈) |
| 8 | 1, 7 | wunrn 10769 |
. . . . 5
⊢ (𝜑 → ran (Hom ‘𝐷) ∈ 𝑈) |
| 9 | 1, 8 | wununi 10746 |
. . . 4
⊢ (𝜑 → ∪ ran (Hom ‘𝐷) ∈ 𝑈) |
| 10 | | baseid 17250 |
. . . . 5
⊢ Base =
Slot (Base‘ndx) |
| 11 | 10, 1, 2 | wunstr 17225 |
. . . 4
⊢ (𝜑 → (Base‘𝐶) ∈ 𝑈) |
| 12 | 1, 9, 11 | wunmap 10766 |
. . 3
⊢ (𝜑 → (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) ∈ 𝑈) |
| 13 | 1, 12 | wunpw 10747 |
. 2
⊢ (𝜑 → 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) ∈ 𝑈) |
| 14 | | fvex 6919 |
. . . . . 6
⊢
(1st ‘𝑓) ∈ V |
| 15 | | fvex 6919 |
. . . . . . . . 9
⊢
(1st ‘𝑔) ∈ V |
| 16 | | ovex 7464 |
. . . . . . . . . . . 12
⊢ (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) ∈ V |
| 17 | | ssrab2 4080 |
. . . . . . . . . . . . 13
⊢ {𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ⊆ X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) |
| 18 | | ovssunirn 7467 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ⊆ ∪ ran
(Hom ‘𝐷) |
| 19 | 18 | rgenw 3065 |
. . . . . . . . . . . . . . 15
⊢
∀𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ⊆ ∪ ran
(Hom ‘𝐷) |
| 20 | | ss2ixp 8950 |
. . . . . . . . . . . . . . 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 6919 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝐶)
∈ V |
| 23 | | fvex 6919 |
. . . . . . . . . . . . . . . . 17
⊢ (Hom
‘𝐷) ∈
V |
| 24 | 23 | rnex 7932 |
. . . . . . . . . . . . . . . 16
⊢ ran (Hom
‘𝐷) ∈
V |
| 25 | 24 | uniex 7761 |
. . . . . . . . . . . . . . 15
⊢ ∪ ran (Hom ‘𝐷) ∈ V |
| 26 | 22, 25 | ixpconst 8947 |
. . . . . . . . . . . . . 14
⊢ X𝑥 ∈
(Base‘𝐶)∪ ran (Hom ‘𝐷) = (∪ ran (Hom
‘𝐷)
↑m (Base‘𝐶)) |
| 27 | 21, 26 | sseqtri 4032 |
. . . . . . . . . . . . 13
⊢ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ⊆ (∪ ran
(Hom ‘𝐷)
↑m (Base‘𝐶)) |
| 28 | 17, 27 | sstri 3993 |
. . . . . . . . . . . 12
⊢ {𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ⊆ (∪ ran
(Hom ‘𝐷)
↑m (Base‘𝐶)) |
| 29 | 16, 28 | elpwi2 5335 |
. . . . . . . . . . 11
⊢ {𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶)) |
| 30 | 29 | sbcth 3803 |
. . . . . . . . . 10
⊢
((1st ‘𝑔) ∈ V → [(1st
‘𝑔) / 𝑠]{𝑎 ∈ X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶))) |
| 31 | | sbcel1g 4416 |
. . . . . . . . . 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 232 |
. . . . . . . . 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 3803 |
. . . . . . 7
⊢
((1st ‘𝑓) ∈ V → [(1st
‘𝑓) / 𝑟]⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ 𝒫 (∪ ran (Hom ‘𝐷) ↑m (Base‘𝐶))) |
| 35 | | sbcel1g 4416 |
. . . . . . 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 232 |
. . . . . 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 3066 |
. . . 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 17994 |
. . . . 5
⊢ (𝐶 Nat 𝐷) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑓) / 𝑟⦌⦋(1st
‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈
(Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘𝑧)) = (((𝑥(2nd ‘𝑔)𝑦)‘𝑧)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))}) |
| 45 | 44 | fmpo 8093 |
. . . 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 230 |
. . 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 10767 |
1
⊢ (𝜑 → (𝐶 Nat 𝐷) ∈ 𝑈) |