Step | Hyp | Ref
| Expression |
1 | | xpccofval.t |
. . . 4
⊢ 𝑇 = (𝐶 ×_{c} 𝐷) |
2 | | eqid 2621 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) |
3 | | eqid 2621 |
. . . 4
⊢
(Base‘𝐷) =
(Base‘𝐷) |
4 | | eqid 2621 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
5 | | eqid 2621 |
. . . 4
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
6 | | xpccofval.o1 |
. . . 4
⊢ · =
(comp‘𝐶) |
7 | | xpccofval.o2 |
. . . 4
⊢ ∙ =
(comp‘𝐷) |
8 | | simpl 473 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐶 ∈ V) |
9 | | simpr 477 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐷 ∈ V) |
10 | | xpccofval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑇) |
11 | 1, 2, 3 | xpcbas 16739 |
. . . . . 6
⊢
((Base‘𝐶)
× (Base‘𝐷)) =
(Base‘𝑇) |
12 | 10, 11 | eqtr4i 2646 |
. . . . 5
⊢ 𝐵 = ((Base‘𝐶) × (Base‘𝐷)) |
13 | 12 | a1i 11 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐵 = ((Base‘𝐶) × (Base‘𝐷))) |
14 | | xpccofval.k |
. . . . . 6
⊢ 𝐾 = (Hom ‘𝑇) |
15 | 1, 10, 4, 5, 14 | xpchomfval 16740 |
. . . . 5
⊢ 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1^{st} ‘𝑢)(Hom ‘𝐶)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝐷)(2^{nd} ‘𝑣)))) |
16 | 15 | a1i 11 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1^{st} ‘𝑢)(Hom ‘𝐶)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝐷)(2^{nd} ‘𝑣))))) |
17 | | eqidd 2622 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))) |
18 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 13,
16, 17 | xpcval 16738 |
. . 3
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑇 = {⟨(Base‘ndx),
𝐵⟩, ⟨(Hom
‘ndx), 𝐾⟩,
⟨(comp‘ndx), (𝑥
∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩}) |
19 | | catstr 16538 |
. . 3
⊢
{⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐾⟩, ⟨(comp‘ndx),
(𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩} Struct ⟨1, ;15⟩ |
20 | | ccoid 15998 |
. . 3
⊢ comp =
Slot (comp‘ndx) |
21 | | snsstp3 4317 |
. . 3
⊢
{⟨(comp‘ndx), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩} ⊆
{⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐾⟩, ⟨(comp‘ndx),
(𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩} |
22 | | fvex 6158 |
. . . . . . 7
⊢
(Base‘𝑇)
∈ V |
23 | 10, 22 | eqeltri 2694 |
. . . . . 6
⊢ 𝐵 ∈ V |
24 | 23, 23 | xpex 6915 |
. . . . 5
⊢ (𝐵 × 𝐵) ∈ V |
25 | 24, 23 | mpt2ex 7192 |
. . . 4
⊢ (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) ∈ V |
26 | 25 | a1i 11 |
. . 3
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) ∈ V) |
27 | | xpccofval.o |
. . 3
⊢ 𝑂 = (comp‘𝑇) |
28 | 18, 19, 20, 21, 26, 27 | strfv3 15829 |
. 2
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))) |
29 | | mpt20 6678 |
. . . 4
⊢ (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑔 ∈ ((2^{nd}
‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) = ∅ |
30 | 29 | eqcomi 2630 |
. . 3
⊢ ∅ =
(𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑔 ∈ ((2^{nd}
‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) |
31 | | fnxpc 16737 |
. . . . . . . 8
⊢
×_{c} Fn (V × V) |
32 | | fndm 5948 |
. . . . . . . 8
⊢ (
×_{c} Fn (V × V) → dom
×_{c} = (V × V)) |
33 | 31, 32 | ax-mp 5 |
. . . . . . 7
⊢ dom
×_{c} = (V × V) |
34 | 33 | ndmov 6771 |
. . . . . 6
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝐶 ×_{c}
𝐷) =
∅) |
35 | 1, 34 | syl5eq 2667 |
. . . . 5
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑇 = ∅) |
36 | 35 | fveq2d 6152 |
. . . 4
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) →
(comp‘𝑇) =
(comp‘∅)) |
37 | 20 | str0 15832 |
. . . 4
⊢ ∅ =
(comp‘∅) |
38 | 36, 27, 37 | 3eqtr4g 2680 |
. . 3
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑂 = ∅) |
39 | 35 | fveq2d 6152 |
. . . . . . 7
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) →
(Base‘𝑇) =
(Base‘∅)) |
40 | | base0 15833 |
. . . . . . 7
⊢ ∅ =
(Base‘∅) |
41 | 39, 10, 40 | 3eqtr4g 2680 |
. . . . . 6
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐵 = ∅) |
42 | 41 | xpeq2d 5099 |
. . . . 5
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝐵 × 𝐵) = (𝐵 × ∅)) |
43 | | xp0 5511 |
. . . . 5
⊢ (𝐵 × ∅) =
∅ |
44 | 42, 43 | syl6eq 2671 |
. . . 4
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝐵 × 𝐵) = ∅) |
45 | | eqidd 2622 |
. . . 4
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑔 ∈ ((2^{nd}
‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) = (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) |
46 | 44, 41, 45 | mpt2eq123dv 6670 |
. . 3
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) = (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))) |
47 | 30, 38, 46 | 3eqtr4a 2681 |
. 2
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))) |
48 | 28, 47 | pm2.61i 176 |
1
⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) |