| Step | Hyp | Ref
| Expression |
| 1 | | wunfunc.1 |
. 2
⊢ (𝜑 → 𝑈 ∈ WUni) |
| 2 | | baseid 17250 |
. . . . 5
⊢ Base =
Slot (Base‘ndx) |
| 3 | | wunfunc.3 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑈) |
| 4 | 2, 1, 3 | wunstr 17225 |
. . . 4
⊢ (𝜑 → (Base‘𝐷) ∈ 𝑈) |
| 5 | | wunfunc.2 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑈) |
| 6 | 2, 1, 5 | wunstr 17225 |
. . . 4
⊢ (𝜑 → (Base‘𝐶) ∈ 𝑈) |
| 7 | 1, 4, 6 | wunmap 10766 |
. . 3
⊢ (𝜑 → ((Base‘𝐷) ↑m
(Base‘𝐶)) ∈
𝑈) |
| 8 | | homid 17456 |
. . . . . . . . 9
⊢ Hom =
Slot (Hom ‘ndx) |
| 9 | 8, 1, 5 | wunstr 17225 |
. . . . . . . 8
⊢ (𝜑 → (Hom ‘𝐶) ∈ 𝑈) |
| 10 | 1, 9 | wunrn 10769 |
. . . . . . 7
⊢ (𝜑 → ran (Hom ‘𝐶) ∈ 𝑈) |
| 11 | 1, 10 | wununi 10746 |
. . . . . 6
⊢ (𝜑 → ∪ ran (Hom ‘𝐶) ∈ 𝑈) |
| 12 | 8, 1, 3 | wunstr 17225 |
. . . . . . . 8
⊢ (𝜑 → (Hom ‘𝐷) ∈ 𝑈) |
| 13 | 1, 12 | wunrn 10769 |
. . . . . . 7
⊢ (𝜑 → ran (Hom ‘𝐷) ∈ 𝑈) |
| 14 | 1, 13 | wununi 10746 |
. . . . . 6
⊢ (𝜑 → ∪ ran (Hom ‘𝐷) ∈ 𝑈) |
| 15 | 1, 11, 14 | wunxp 10764 |
. . . . 5
⊢ (𝜑 → (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) ∈
𝑈) |
| 16 | 1, 15 | wunpw 10747 |
. . . 4
⊢ (𝜑 → 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) ∈
𝑈) |
| 17 | 1, 6, 6 | wunxp 10764 |
. . . 4
⊢ (𝜑 → ((Base‘𝐶) × (Base‘𝐶)) ∈ 𝑈) |
| 18 | 1, 16, 17 | wunmap 10766 |
. . 3
⊢ (𝜑 → (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶))) ∈ 𝑈) |
| 19 | 1, 7, 18 | wunxp 10764 |
. 2
⊢ (𝜑 → (((Base‘𝐷) ↑m
(Base‘𝐶)) ×
(𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶)))) ∈ 𝑈) |
| 20 | | relfunc 17907 |
. . . 4
⊢ Rel
(𝐶 Func 𝐷) |
| 21 | 20 | a1i 11 |
. . 3
⊢ (𝜑 → Rel (𝐶 Func 𝐷)) |
| 22 | | df-br 5144 |
. . . 4
⊢ (𝑓(𝐶 Func 𝐷)𝑔 ↔ 〈𝑓, 𝑔〉 ∈ (𝐶 Func 𝐷)) |
| 23 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 24 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 25 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑓(𝐶 Func 𝐷)𝑔) |
| 26 | 23, 24, 25 | funcf1 17911 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑓:(Base‘𝐶)⟶(Base‘𝐷)) |
| 27 | | fvex 6919 |
. . . . . . . 8
⊢
(Base‘𝐷)
∈ V |
| 28 | | fvex 6919 |
. . . . . . . 8
⊢
(Base‘𝐶)
∈ V |
| 29 | 27, 28 | elmap 8911 |
. . . . . . 7
⊢ (𝑓 ∈ ((Base‘𝐷) ↑m
(Base‘𝐶)) ↔
𝑓:(Base‘𝐶)⟶(Base‘𝐷)) |
| 30 | 26, 29 | sylibr 234 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑓 ∈ ((Base‘𝐷) ↑m (Base‘𝐶))) |
| 31 | | mapsspw 8918 |
. . . . . . . . . . 11
⊢ (((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧)) ⊆ 𝒫 (((Hom
‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) |
| 32 | | fvssunirn 6939 |
. . . . . . . . . . . . 13
⊢ ((Hom
‘𝐶)‘𝑧) ⊆ ∪ ran (Hom ‘𝐶) |
| 33 | | ovssunirn 7467 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ⊆ ∪ ran (Hom ‘𝐷) |
| 34 | | xpss12 5700 |
. . . . . . . . . . . . 13
⊢ ((((Hom
‘𝐶)‘𝑧) ⊆ ∪ ran (Hom ‘𝐶) ∧ ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ⊆ ∪ ran (Hom ‘𝐷)) → (((Hom ‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) ⊆ (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))) |
| 35 | 32, 33, 34 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (((Hom
‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) ⊆ (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) |
| 36 | 35 | sspwi 4612 |
. . . . . . . . . . 11
⊢ 𝒫
(((Hom ‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) ⊆ 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) |
| 37 | 31, 36 | sstri 3993 |
. . . . . . . . . 10
⊢ (((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧)) ⊆ 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) |
| 38 | 37 | rgenw 3065 |
. . . . . . . . 9
⊢
∀𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))(((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧)) ⊆ 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) |
| 39 | | ss2ixp 8950 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))(((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧)) ⊆ 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) →
X𝑧
∈ ((Base‘𝐶)
× (Base‘𝐶))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧)) ⊆ X𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))𝒫
(∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))) |
| 40 | 38, 39 | ax-mp 5 |
. . . . . . . 8
⊢ X𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))(((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧)) ⊆ X𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))𝒫
(∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) |
| 41 | 28, 28 | xpex 7773 |
. . . . . . . . 9
⊢
((Base‘𝐶)
× (Base‘𝐶))
∈ V |
| 42 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (Hom
‘𝐶) ∈
V |
| 43 | 42 | rnex 7932 |
. . . . . . . . . . . 12
⊢ ran (Hom
‘𝐶) ∈
V |
| 44 | 43 | uniex 7761 |
. . . . . . . . . . 11
⊢ ∪ ran (Hom ‘𝐶) ∈ V |
| 45 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (Hom
‘𝐷) ∈
V |
| 46 | 45 | rnex 7932 |
. . . . . . . . . . . 12
⊢ ran (Hom
‘𝐷) ∈
V |
| 47 | 46 | uniex 7761 |
. . . . . . . . . . 11
⊢ ∪ ran (Hom ‘𝐷) ∈ V |
| 48 | 44, 47 | xpex 7773 |
. . . . . . . . . 10
⊢ (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) ∈
V |
| 49 | 48 | pwex 5380 |
. . . . . . . . 9
⊢ 𝒫
(∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) ∈
V |
| 50 | 41, 49 | ixpconst 8947 |
. . . . . . . 8
⊢ X𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))𝒫
(∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) =
(𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶))) |
| 51 | 40, 50 | sseqtri 4032 |
. . . . . . 7
⊢ X𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))(((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧)) ⊆ (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶))) |
| 52 | | eqid 2737 |
. . . . . . . 8
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 53 | | eqid 2737 |
. . . . . . . 8
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 54 | 23, 52, 53, 25 | funcixp 17912 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑔 ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧))) |
| 55 | 51, 54 | sselid 3981 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑔 ∈ (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶)))) |
| 56 | 30, 55 | opelxpd 5724 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 〈𝑓, 𝑔〉 ∈ (((Base‘𝐷) ↑m (Base‘𝐶)) × (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶))))) |
| 57 | 56 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑓(𝐶 Func 𝐷)𝑔 → 〈𝑓, 𝑔〉 ∈ (((Base‘𝐷) ↑m (Base‘𝐶)) × (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶)))))) |
| 58 | 22, 57 | biimtrrid 243 |
. . 3
⊢ (𝜑 → (〈𝑓, 𝑔〉 ∈ (𝐶 Func 𝐷) → 〈𝑓, 𝑔〉 ∈ (((Base‘𝐷) ↑m (Base‘𝐶)) × (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶)))))) |
| 59 | 21, 58 | relssdv 5798 |
. 2
⊢ (𝜑 → (𝐶 Func 𝐷) ⊆ (((Base‘𝐷) ↑m (Base‘𝐶)) × (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶))))) |
| 60 | 1, 19, 59 | wunss 10752 |
1
⊢ (𝜑 → (𝐶 Func 𝐷) ∈ 𝑈) |