Step | Hyp | Ref
| Expression |
1 | | xpccofval.t |
. . . 4
⊢ 𝑇 = (𝐶 ×c 𝐷) |
2 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) |
3 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐷) =
(Base‘𝐷) |
4 | | eqid 2738 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
5 | | eqid 2738 |
. . . 4
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
6 | | xpccofval.o1 |
. . . 4
⊢ · =
(comp‘𝐶) |
7 | | xpccofval.o2 |
. . . 4
⊢ ∙ =
(comp‘𝐷) |
8 | | simpl 486 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐶 ∈ V) |
9 | | simpr 488 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐷 ∈ V) |
10 | | xpccofval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑇) |
11 | 1, 2, 3 | xpcbas 17544 |
. . . . . 6
⊢
((Base‘𝐶)
× (Base‘𝐷)) =
(Base‘𝑇) |
12 | 10, 11 | eqtr4i 2764 |
. . . . 5
⊢ 𝐵 = ((Base‘𝐶) × (Base‘𝐷)) |
13 | 12 | a1i 11 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐵 = ((Base‘𝐶) × (Base‘𝐷))) |
14 | | xpccofval.k |
. . . . . 6
⊢ 𝐾 = (Hom ‘𝑇) |
15 | 1, 10, 4, 5, 14 | xpchomfval 17545 |
. . . . 5
⊢ 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣)))) |
16 | 15 | a1i 11 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))) |
17 | | eqidd 2739 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉)) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉))) |
18 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 13,
16, 17 | xpcval 17543 |
. . 3
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑇 = {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝐾〉,
〈(comp‘ndx), (𝑥
∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉))〉}) |
19 | | catstr 17332 |
. . 3
⊢
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐾〉, 〈(comp‘ndx),
(𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} Struct 〈1, ;15〉 |
20 | | ccoid 16793 |
. . 3
⊢ comp =
Slot (comp‘ndx) |
21 | | snsstp3 4706 |
. . 3
⊢
{〈(comp‘ndx), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} ⊆
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐾〉, 〈(comp‘ndx),
(𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} |
22 | 10 | fvexi 6688 |
. . . . . 6
⊢ 𝐵 ∈ V |
23 | 22, 22 | xpex 7494 |
. . . . 5
⊢ (𝐵 × 𝐵) ∈ V |
24 | 23, 22 | mpoex 7803 |
. . . 4
⊢ (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉)) ∈ V |
25 | 24 | a1i 11 |
. . 3
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉)) ∈ V) |
26 | | xpccofval.o |
. . 3
⊢ 𝑂 = (comp‘𝑇) |
27 | 18, 19, 20, 21, 25, 26 | strfv3 16635 |
. 2
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉))) |
28 | | fnxpc 17542 |
. . . . . . . 8
⊢
×c Fn (V × V) |
29 | 28 | fndmi 6441 |
. . . . . . 7
⊢ dom
×c = (V × V) |
30 | 29 | ndmov 7348 |
. . . . . 6
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝐶 ×c
𝐷) =
∅) |
31 | 1, 30 | syl5eq 2785 |
. . . . 5
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑇 = ∅) |
32 | 31 | fveq2d 6678 |
. . . 4
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) →
(comp‘𝑇) =
(comp‘∅)) |
33 | 20 | str0 16638 |
. . . 4
⊢ ∅ =
(comp‘∅) |
34 | 32, 26, 33 | 3eqtr4g 2798 |
. . 3
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑂 = ∅) |
35 | 31 | fveq2d 6678 |
. . . . . 6
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) →
(Base‘𝑇) =
(Base‘∅)) |
36 | | base0 16639 |
. . . . . 6
⊢ ∅ =
(Base‘∅) |
37 | 35, 10, 36 | 3eqtr4g 2798 |
. . . . 5
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐵 = ∅) |
38 | 37 | olcd 873 |
. . . 4
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → ((𝐵 × 𝐵) = ∅ ∨ 𝐵 = ∅)) |
39 | | 0mpo0 7251 |
. . . 4
⊢ (((𝐵 × 𝐵) = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉)) = ∅) |
40 | 38, 39 | syl 17 |
. . 3
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉)) = ∅) |
41 | 34, 40 | eqtr4d 2776 |
. 2
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉))) |
42 | 27, 41 | pm2.61i 185 |
1
⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉)) |