Step | Hyp | Ref
| Expression |
1 | | xpcbas.t |
. . . . 5
⊢ 𝑇 = (𝐶 ×c 𝐷) |
2 | | xpcbas.x |
. . . . 5
⊢ 𝑋 = (Base‘𝐶) |
3 | | xpcbas.y |
. . . . 5
⊢ 𝑌 = (Base‘𝐷) |
4 | | eqid 2610 |
. . . . 5
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
5 | | eqid 2610 |
. . . . 5
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
6 | | eqid 2610 |
. . . . 5
⊢
(comp‘𝐶) =
(comp‘𝐶) |
7 | | eqid 2610 |
. . . . 5
⊢
(comp‘𝐷) =
(comp‘𝐷) |
8 | | simpl 472 |
. . . . 5
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐶 ∈ V) |
9 | | simpr 476 |
. . . . 5
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐷 ∈ V) |
10 | | eqidd 2611 |
. . . . 5
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) = (𝑋 × 𝑌)) |
11 | | eqidd 2611 |
. . . . 5
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣)))) = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))) |
12 | | eqidd 2611 |
. . . . 5
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑥 ∈ ((𝑋 × 𝑌) × (𝑋 × 𝑌)), 𝑦 ∈ (𝑋 × 𝑌) ↦ (𝑔 ∈ ((2nd ‘𝑥)(𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))𝑦), 𝑓 ∈ ((𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝐶)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))〉)) = (𝑥 ∈ ((𝑋 × 𝑌) × (𝑋 × 𝑌)), 𝑦 ∈ (𝑋 × 𝑌) ↦ (𝑔 ∈ ((2nd ‘𝑥)(𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))𝑦), 𝑓 ∈ ((𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝐶)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))〉))) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | xpcval 16640 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑇 = {〈(Base‘ndx),
(𝑋 × 𝑌)〉, 〈(Hom ‘ndx),
(𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))〉, 〈(comp‘ndx), (𝑥 ∈ ((𝑋 × 𝑌) × (𝑋 × 𝑌)), 𝑦 ∈ (𝑋 × 𝑌) ↦ (𝑔 ∈ ((2nd ‘𝑥)(𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))𝑦), 𝑓 ∈ ((𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝐶)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉}) |
14 | | catstr 16440 |
. . . 4
⊢
{〈(Base‘ndx), (𝑋 × 𝑌)〉, 〈(Hom ‘ndx), (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))〉, 〈(comp‘ndx), (𝑥 ∈ ((𝑋 × 𝑌) × (𝑋 × 𝑌)), 𝑦 ∈ (𝑋 × 𝑌) ↦ (𝑔 ∈ ((2nd ‘𝑥)(𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))𝑦), 𝑓 ∈ ((𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝐶)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} Struct 〈1, ;15〉 |
15 | | baseid 15747 |
. . . 4
⊢ Base =
Slot (Base‘ndx) |
16 | | snsstp1 4287 |
. . . 4
⊢
{〈(Base‘ndx), (𝑋 × 𝑌)〉} ⊆ {〈(Base‘ndx),
(𝑋 × 𝑌)〉, 〈(Hom ‘ndx),
(𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))〉, 〈(comp‘ndx), (𝑥 ∈ ((𝑋 × 𝑌) × (𝑋 × 𝑌)), 𝑦 ∈ (𝑋 × 𝑌) ↦ (𝑔 ∈ ((2nd ‘𝑥)(𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))𝑦), 𝑓 ∈ ((𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝐶)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} |
17 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
18 | 2, 17 | eqeltri 2684 |
. . . . . 6
⊢ 𝑋 ∈ V |
19 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐷)
∈ V |
20 | 3, 19 | eqeltri 2684 |
. . . . . 6
⊢ 𝑌 ∈ V |
21 | 18, 20 | xpex 6860 |
. . . . 5
⊢ (𝑋 × 𝑌) ∈ V |
22 | 21 | a1i 11 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) ∈ V) |
23 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑇) =
(Base‘𝑇) |
24 | 13, 14, 15, 16, 22, 23 | strfv3 15736 |
. . 3
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) →
(Base‘𝑇) = (𝑋 × 𝑌)) |
25 | 24 | eqcomd 2616 |
. 2
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) = (Base‘𝑇)) |
26 | | base0 15740 |
. . 3
⊢ ∅ =
(Base‘∅) |
27 | | fvprc 6097 |
. . . . . 6
⊢ (¬
𝐶 ∈ V →
(Base‘𝐶) =
∅) |
28 | 2, 27 | syl5eq 2656 |
. . . . 5
⊢ (¬
𝐶 ∈ V → 𝑋 = ∅) |
29 | | fvprc 6097 |
. . . . . 6
⊢ (¬
𝐷 ∈ V →
(Base‘𝐷) =
∅) |
30 | 3, 29 | syl5eq 2656 |
. . . . 5
⊢ (¬
𝐷 ∈ V → 𝑌 = ∅) |
31 | 28, 30 | orim12i 537 |
. . . 4
⊢ ((¬
𝐶 ∈ V ∨ ¬ 𝐷 ∈ V) → (𝑋 = ∅ ∨ 𝑌 = ∅)) |
32 | | ianor 508 |
. . . 4
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) ↔ (¬ 𝐶 ∈ V ∨ ¬ 𝐷 ∈ V)) |
33 | | xpeq0 5473 |
. . . 4
⊢ ((𝑋 × 𝑌) = ∅ ↔ (𝑋 = ∅ ∨ 𝑌 = ∅)) |
34 | 31, 32, 33 | 3imtr4i 280 |
. . 3
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) = ∅) |
35 | | fnxpc 16639 |
. . . . . . 7
⊢
×c Fn (V × V) |
36 | | fndm 5904 |
. . . . . . 7
⊢ (
×c Fn (V × V) → dom
×c = (V × V)) |
37 | 35, 36 | ax-mp 5 |
. . . . . 6
⊢ dom
×c = (V × V) |
38 | 37 | ndmov 6716 |
. . . . 5
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝐶 ×c
𝐷) =
∅) |
39 | 1, 38 | syl5eq 2656 |
. . . 4
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑇 = ∅) |
40 | 39 | fveq2d 6107 |
. . 3
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) →
(Base‘𝑇) =
(Base‘∅)) |
41 | 26, 34, 40 | 3eqtr4a 2670 |
. 2
⊢ (¬
(𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) = (Base‘𝑇)) |
42 | 25, 41 | pm2.61i 175 |
1
⊢ (𝑋 × 𝑌) = (Base‘𝑇) |