Step | Hyp | Ref
| Expression |
1 | | xpchomfval.t |
. . . 4
⊢ 𝑇 = (𝐶 ×c 𝐷) |
2 | | eqid 2610 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) |
3 | | eqid 2610 |
. . . 4
⊢
(Base‘𝐷) =
(Base‘𝐷) |
4 | | xpchomfval.h |
. . . 4
⊢ 𝐻 = (Hom ‘𝐶) |
5 | | xpchomfval.j |
. . . 4
⊢ 𝐽 = (Hom ‘𝐷) |
6 | | eqid 2610 |
. . . 4
⊢
(comp‘𝐶) =
(comp‘𝐶) |
7 | | eqid 2610 |
. . . 4
⊢
(comp‘𝐷) =
(comp‘𝐷) |
8 | | simpl 472 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐶 ∈ V) |
9 | | simpr 476 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐷 ∈ V) |
10 | | xpchomfval.y |
. . . . . 6
⊢ 𝐵 = (Base‘𝑇) |
11 | 1, 2, 3 | xpcbas 16641 |
. . . . . 6
⊢
((Base‘𝐶)
× (Base‘𝐷)) =
(Base‘𝑇) |
12 | 10, 11 | eqtr4i 2635 |
. . . . 5
⊢ 𝐵 = ((Base‘𝐶) × (Base‘𝐷)) |
13 | 12 | a1i 11 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐵 = ((Base‘𝐶) × (Base‘𝐷))) |
14 | | eqidd 2611 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣)))) = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))) |
15 | | eqidd 2611 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)(𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))𝑦), 𝑓 ∈ ((𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝐶)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))〉)) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)(𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))𝑦), 𝑓 ∈ ((𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝐶)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))〉))) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 13,
14, 15 | xpcval 16640 |
. . 3
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑇 = {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), (𝑢 ∈
𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))〉, 〈(comp‘ndx), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)(𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))𝑦), 𝑓 ∈ ((𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝐶)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉}) |
17 | | catstr 16440 |
. . 3
⊢
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))〉, 〈(comp‘ndx), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)(𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))𝑦), 𝑓 ∈ ((𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝐶)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} Struct 〈1, ;15〉 |
18 | | homid 15898 |
. . 3
⊢ Hom =
Slot (Hom ‘ndx) |
19 | | snsstp2 4288 |
. . 3
⊢
{〈(Hom ‘ndx), (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))〉} ⊆ {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), (𝑢 ∈
𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))〉, 〈(comp‘ndx), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)(𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))𝑦), 𝑓 ∈ ((𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝐶)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} |
20 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑇)
∈ V |
21 | 10, 20 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
22 | 21, 21 | mpt2ex 7136 |
. . . 4
⊢ (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣)))) ∈ V |
23 | 22 | a1i 11 |
. . 3
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣)))) ∈ V) |
24 | | xpchomfval.k |
. . 3
⊢ 𝐾 = (Hom ‘𝑇) |
25 | 16, 17, 18, 19, 23, 24 | strfv3 15736 |
. 2
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))) |
26 | | mpt20 6623 |
. . . 4
⊢ (𝑢 ∈ ∅, 𝑣 ∈ ∅ ↦
(((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣)))) = ∅ |
27 | 26 | eqcomi 2619 |
. . 3
⊢ ∅ =
(𝑢 ∈ ∅, 𝑣 ∈ ∅ ↦
(((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣)))) |
28 | | fnxpc 16639 |
. . . . . . . 8
⊢
×c Fn (V × V) |
29 | | fndm 5904 |
. . . . . . . 8
⊢ (
×c Fn (V × V) → dom
×c = (V × V)) |
30 | 28, 29 | ax-mp 5 |
. . . . . . 7
⊢ dom
×c = (V × V) |
31 | 30 | ndmov 6716 |
. . . . . 6
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝐶 ×c
𝐷) =
∅) |
32 | 1, 31 | syl5eq 2656 |
. . . . 5
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑇 = ∅) |
33 | 32 | fveq2d 6107 |
. . . 4
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → (Hom
‘𝑇) = (Hom
‘∅)) |
34 | 18 | str0 15739 |
. . . 4
⊢ ∅ =
(Hom ‘∅) |
35 | 33, 24, 34 | 3eqtr4g 2669 |
. . 3
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐾 = ∅) |
36 | 32 | fveq2d 6107 |
. . . . 5
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) →
(Base‘𝑇) =
(Base‘∅)) |
37 | | base0 15740 |
. . . . 5
⊢ ∅ =
(Base‘∅) |
38 | 36, 10, 37 | 3eqtr4g 2669 |
. . . 4
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐵 = ∅) |
39 | | eqidd 2611 |
. . . 4
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) →
(((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))) = (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣)))) |
40 | 38, 38, 39 | mpt2eq123dv 6615 |
. . 3
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣)))) = (𝑢 ∈ ∅, 𝑣 ∈ ∅ ↦ (((1st
‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))) |
41 | 27, 35, 40 | 3eqtr4a 2670 |
. 2
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))) |
42 | 25, 41 | pm2.61i 175 |
1
⊢ 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣)))) |