Step | Hyp | Ref
| Expression |
1 | | wunfunc.1 |
. 2
⊢ (𝜑 → 𝑈 ∈ WUni) |
2 | | df-base 16941 |
. . . . 5
⊢ Base =
Slot 1 |
3 | | wunfunc.3 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑈) |
4 | 2, 1, 3 | wunstr 16917 |
. . . 4
⊢ (𝜑 → (Base‘𝐷) ∈ 𝑈) |
5 | | wunfunc.2 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑈) |
6 | 2, 1, 5 | wunstr 16917 |
. . . 4
⊢ (𝜑 → (Base‘𝐶) ∈ 𝑈) |
7 | 1, 4, 6 | wunmap 10510 |
. . 3
⊢ (𝜑 → ((Base‘𝐷) ↑m
(Base‘𝐶)) ∈
𝑈) |
8 | | df-hom 17014 |
. . . . . . . . 9
⊢ Hom =
Slot ;14 |
9 | 8, 1, 5 | wunstr 16917 |
. . . . . . . 8
⊢ (𝜑 → (Hom ‘𝐶) ∈ 𝑈) |
10 | 1, 9 | wunrn 10513 |
. . . . . . 7
⊢ (𝜑 → ran (Hom ‘𝐶) ∈ 𝑈) |
11 | 1, 10 | wununi 10490 |
. . . . . 6
⊢ (𝜑 → ∪ ran (Hom ‘𝐶) ∈ 𝑈) |
12 | 8, 1, 3 | wunstr 16917 |
. . . . . . . 8
⊢ (𝜑 → (Hom ‘𝐷) ∈ 𝑈) |
13 | 1, 12 | wunrn 10513 |
. . . . . . 7
⊢ (𝜑 → ran (Hom ‘𝐷) ∈ 𝑈) |
14 | 1, 13 | wununi 10490 |
. . . . . 6
⊢ (𝜑 → ∪ ran (Hom ‘𝐷) ∈ 𝑈) |
15 | 1, 11, 14 | wunxp 10508 |
. . . . 5
⊢ (𝜑 → (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) ∈
𝑈) |
16 | 1, 15 | wunpw 10491 |
. . . 4
⊢ (𝜑 → 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) ∈
𝑈) |
17 | 1, 6, 6 | wunxp 10508 |
. . . 4
⊢ (𝜑 → ((Base‘𝐶) × (Base‘𝐶)) ∈ 𝑈) |
18 | 1, 16, 17 | wunmap 10510 |
. . 3
⊢ (𝜑 → (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶))) ∈ 𝑈) |
19 | 1, 7, 18 | wunxp 10508 |
. 2
⊢ (𝜑 → (((Base‘𝐷) ↑m
(Base‘𝐶)) ×
(𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶)))) ∈ 𝑈) |
20 | | relfunc 17605 |
. . . 4
⊢ Rel
(𝐶 Func 𝐷) |
21 | 20 | a1i 11 |
. . 3
⊢ (𝜑 → Rel (𝐶 Func 𝐷)) |
22 | | df-br 5078 |
. . . 4
⊢ (𝑓(𝐶 Func 𝐷)𝑔 ↔ 〈𝑓, 𝑔〉 ∈ (𝐶 Func 𝐷)) |
23 | | eqid 2733 |
. . . . . . . 8
⊢
(Base‘𝐶) =
(Base‘𝐶) |
24 | | eqid 2733 |
. . . . . . . 8
⊢
(Base‘𝐷) =
(Base‘𝐷) |
25 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑓(𝐶 Func 𝐷)𝑔) |
26 | 23, 24, 25 | funcf1 17609 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑓:(Base‘𝐶)⟶(Base‘𝐷)) |
27 | | fvex 6805 |
. . . . . . . 8
⊢
(Base‘𝐷)
∈ V |
28 | | fvex 6805 |
. . . . . . . 8
⊢
(Base‘𝐶)
∈ V |
29 | 27, 28 | elmap 8679 |
. . . . . . 7
⊢ (𝑓 ∈ ((Base‘𝐷) ↑m
(Base‘𝐶)) ↔
𝑓:(Base‘𝐶)⟶(Base‘𝐷)) |
30 | 26, 29 | sylibr 233 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑓 ∈ ((Base‘𝐷) ↑m (Base‘𝐶))) |
31 | | mapsspw 8686 |
. . . . . . . . . . 11
⊢ (((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧)) ⊆ 𝒫 (((Hom
‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) |
32 | | fvssunirn 6823 |
. . . . . . . . . . . . 13
⊢ ((Hom
‘𝐶)‘𝑧) ⊆ ∪ ran (Hom ‘𝐶) |
33 | | ovssunirn 7331 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ⊆ ∪ ran (Hom ‘𝐷) |
34 | | xpss12 5606 |
. . . . . . . . . . . . 13
⊢ ((((Hom
‘𝐶)‘𝑧) ⊆ ∪ ran (Hom ‘𝐶) ∧ ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ⊆ ∪ ran (Hom ‘𝐷)) → (((Hom ‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) ⊆ (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))) |
35 | 32, 33, 34 | mp2an 688 |
. . . . . . . . . . . 12
⊢ (((Hom
‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) ⊆ (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) |
36 | 35 | sspwi 4550 |
. . . . . . . . . . 11
⊢ 𝒫
(((Hom ‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) ⊆ 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) |
37 | 31, 36 | sstri 3932 |
. . . . . . . . . 10
⊢ (((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧)) ⊆ 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) |
38 | 37 | rgenw 3063 |
. . . . . . . . 9
⊢
∀𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))(((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧)) ⊆ 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) |
39 | | ss2ixp 8718 |
. . . . . . . . 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 7623 |
. . . . . . . . 9
⊢
((Base‘𝐶)
× (Base‘𝐶))
∈ V |
42 | | fvex 6805 |
. . . . . . . . . . . . 13
⊢ (Hom
‘𝐶) ∈
V |
43 | 42 | rnex 7779 |
. . . . . . . . . . . 12
⊢ ran (Hom
‘𝐶) ∈
V |
44 | 43 | uniex 7614 |
. . . . . . . . . . 11
⊢ ∪ ran (Hom ‘𝐶) ∈ V |
45 | | fvex 6805 |
. . . . . . . . . . . . 13
⊢ (Hom
‘𝐷) ∈
V |
46 | 45 | rnex 7779 |
. . . . . . . . . . . 12
⊢ ran (Hom
‘𝐷) ∈
V |
47 | 46 | uniex 7614 |
. . . . . . . . . . 11
⊢ ∪ ran (Hom ‘𝐷) ∈ V |
48 | 44, 47 | xpex 7623 |
. . . . . . . . . 10
⊢ (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) ∈
V |
49 | 48 | pwex 5306 |
. . . . . . . . 9
⊢ 𝒫
(∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) ∈
V |
50 | 41, 49 | ixpconst 8715 |
. . . . . . . 8
⊢ X𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))𝒫
(∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷)) =
(𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶))) |
51 | 40, 50 | sseqtri 3959 |
. . . . . . 7
⊢ X𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))(((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧)) ⊆ (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶))) |
52 | | eqid 2733 |
. . . . . . . 8
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
53 | | eqid 2733 |
. . . . . . . 8
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
54 | 23, 52, 53, 25 | funcixp 17610 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑔 ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧))) |
55 | 51, 54 | sselid 3921 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑔 ∈ (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶)))) |
56 | 30, 55 | opelxpd 5629 |
. . . . 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 | syl5bir 242 |
. . 3
⊢ (𝜑 → (〈𝑓, 𝑔〉 ∈ (𝐶 Func 𝐷) → 〈𝑓, 𝑔〉 ∈ (((Base‘𝐷) ↑m (Base‘𝐶)) × (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶)))))) |
59 | 21, 58 | relssdv 5701 |
. 2
⊢ (𝜑 → (𝐶 Func 𝐷) ⊆ (((Base‘𝐷) ↑m (Base‘𝐶)) × (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran
(Hom ‘𝐷))
↑m ((Base‘𝐶) × (Base‘𝐶))))) |
60 | 1, 19, 59 | wunss 10496 |
1
⊢ (𝜑 → (𝐶 Func 𝐷) ∈ 𝑈) |