Step | Hyp | Ref
| Expression |
1 | | dmexg 7097 |
. . . . . 6
⊢ (𝑥 ∈ V → dom 𝑥 ∈ V) |
2 | 1 | adantl 482 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ V) → dom 𝑥 ∈ V) |
3 | 2 | ralrimiva 2966 |
. . . 4
⊢ (𝐶 ∈ Cat → ∀𝑥 ∈ V dom 𝑥 ∈ V) |
4 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ V ↦ dom 𝑥) = (𝑥 ∈ V ↦ dom 𝑥) |
5 | 4 | fnmpt 6020 |
. . . 4
⊢
(∀𝑥 ∈ V
dom 𝑥 ∈ V →
(𝑥 ∈ V ↦ dom
𝑥) Fn V) |
6 | 3, 5 | syl 17 |
. . 3
⊢ (𝐶 ∈ Cat → (𝑥 ∈ V ↦ dom 𝑥) Fn V) |
7 | | ovex 6678 |
. . . . . . . 8
⊢ (𝑥(Sect‘𝐶)𝑦) ∈ V |
8 | 7 | inex1 4799 |
. . . . . . 7
⊢ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)) ∈ V |
9 | 8 | a1i 11 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)) ∈ V) |
10 | 9 | ralrimivva 2971 |
. . . . 5
⊢ (𝐶 ∈ Cat → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)) ∈ V) |
11 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) |
12 | 11 | fnmpt2 7238 |
. . . . 5
⊢
(∀𝑥 ∈
(Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)) ∈ V → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) Fn ((Base‘𝐶) × (Base‘𝐶))) |
13 | 10, 12 | syl 17 |
. . . 4
⊢ (𝐶 ∈ Cat → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) Fn ((Base‘𝐶) × (Base‘𝐶))) |
14 | | df-inv 16408 |
. . . . . . 7
⊢ Inv =
(𝑐 ∈ Cat ↦
(𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ ((𝑥(Sect‘𝑐)𝑦) ∩ ◡(𝑦(Sect‘𝑐)𝑥)))) |
15 | 14 | a1i 11 |
. . . . . 6
⊢ (𝐶 ∈ Cat → Inv = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ ((𝑥(Sect‘𝑐)𝑦) ∩ ◡(𝑦(Sect‘𝑐)𝑥))))) |
16 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = (Base‘𝐶)) |
17 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐶 → (Sect‘𝑐) = (Sect‘𝐶)) |
18 | 17 | oveqd 6667 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → (𝑥(Sect‘𝑐)𝑦) = (𝑥(Sect‘𝐶)𝑦)) |
19 | 17 | oveqd 6667 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐶 → (𝑦(Sect‘𝑐)𝑥) = (𝑦(Sect‘𝐶)𝑥)) |
20 | 19 | cnveqd 5298 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → ◡(𝑦(Sect‘𝑐)𝑥) = ◡(𝑦(Sect‘𝐶)𝑥)) |
21 | 18, 20 | ineq12d 3815 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → ((𝑥(Sect‘𝑐)𝑦) ∩ ◡(𝑦(Sect‘𝑐)𝑥)) = ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) |
22 | 16, 16, 21 | mpt2eq123dv 6717 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ ((𝑥(Sect‘𝑐)𝑦) ∩ ◡(𝑦(Sect‘𝑐)𝑥))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)))) |
23 | 22 | adantl 482 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ 𝑐 = 𝐶) → (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ ((𝑥(Sect‘𝑐)𝑦) ∩ ◡(𝑦(Sect‘𝑐)𝑥))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)))) |
24 | | id 22 |
. . . . . 6
⊢ (𝐶 ∈ Cat → 𝐶 ∈ Cat) |
25 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝐶)
∈ V |
26 | 25, 25 | pm3.2i 471 |
. . . . . . 7
⊢
((Base‘𝐶)
∈ V ∧ (Base‘𝐶) ∈ V) |
27 | 11 | mpt2exg 7245 |
. . . . . . 7
⊢
(((Base‘𝐶)
∈ V ∧ (Base‘𝐶) ∈ V) → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) ∈ V) |
28 | 26, 27 | mp1i 13 |
. . . . . 6
⊢ (𝐶 ∈ Cat → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) ∈ V) |
29 | 15, 23, 24, 28 | fvmptd 6288 |
. . . . 5
⊢ (𝐶 ∈ Cat →
(Inv‘𝐶) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)))) |
30 | 29 | fneq1d 5981 |
. . . 4
⊢ (𝐶 ∈ Cat →
((Inv‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶)) ↔
(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) Fn ((Base‘𝐶) × (Base‘𝐶)))) |
31 | 13, 30 | mpbird 247 |
. . 3
⊢ (𝐶 ∈ Cat →
(Inv‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶))) |
32 | | ssv 3625 |
. . . 4
⊢ ran
(Inv‘𝐶) ⊆
V |
33 | 32 | a1i 11 |
. . 3
⊢ (𝐶 ∈ Cat → ran
(Inv‘𝐶) ⊆
V) |
34 | | fnco 5999 |
. . 3
⊢ (((𝑥 ∈ V ↦ dom 𝑥) Fn V ∧ (Inv‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)) ∧ ran (Inv‘𝐶) ⊆ V) → ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝐶)) Fn ((Base‘𝐶) × (Base‘𝐶))) |
35 | 6, 31, 33, 34 | syl3anc 1326 |
. 2
⊢ (𝐶 ∈ Cat → ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝐶)) Fn ((Base‘𝐶) × (Base‘𝐶))) |
36 | | isofval 16417 |
. . 3
⊢ (𝐶 ∈ Cat →
(Iso‘𝐶) = ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝐶))) |
37 | 36 | fneq1d 5981 |
. 2
⊢ (𝐶 ∈ Cat →
((Iso‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶)) ↔
((𝑥 ∈ V ↦ dom
𝑥) ∘ (Inv‘𝐶)) Fn ((Base‘𝐶) × (Base‘𝐶)))) |
38 | 35, 37 | mpbird 247 |
1
⊢ (𝐶 ∈ Cat →
(Iso‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶))) |