Step | Hyp | Ref
| Expression |
1 | | relopabv 5726 |
. . . . . 6
⊢ Rel
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ ((Iso‘𝐶)‘〈𝑥, 𝑦〉) ≠ ∅)} |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝐶 ∈ Cat → Rel
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ ((Iso‘𝐶)‘〈𝑥, 𝑦〉) ≠ ∅)}) |
3 | | fveq2 6768 |
. . . . . . . . 9
⊢ (𝑓 = 〈𝑥, 𝑦〉 → ((Iso‘𝐶)‘𝑓) = ((Iso‘𝐶)‘〈𝑥, 𝑦〉)) |
4 | 3 | neeq1d 3003 |
. . . . . . . 8
⊢ (𝑓 = 〈𝑥, 𝑦〉 → (((Iso‘𝐶)‘𝑓) ≠ ∅ ↔ ((Iso‘𝐶)‘〈𝑥, 𝑦〉) ≠ ∅)) |
5 | 4 | rabxp 5632 |
. . . . . . 7
⊢ {𝑓 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∣ ((Iso‘𝐶)‘𝑓) ≠ ∅} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ ((Iso‘𝐶)‘〈𝑥, 𝑦〉) ≠ ∅)} |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝐶 ∈ Cat → {𝑓 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∣ ((Iso‘𝐶)‘𝑓) ≠ ∅} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ ((Iso‘𝐶)‘〈𝑥, 𝑦〉) ≠ ∅)}) |
7 | 6 | releqd 5685 |
. . . . 5
⊢ (𝐶 ∈ Cat → (Rel {𝑓 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∣ ((Iso‘𝐶)‘𝑓) ≠ ∅} ↔ Rel {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ ((Iso‘𝐶)‘〈𝑥, 𝑦〉) ≠ ∅)})) |
8 | 2, 7 | mpbird 256 |
. . . 4
⊢ (𝐶 ∈ Cat → Rel {𝑓 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∣ ((Iso‘𝐶)‘𝑓) ≠ ∅}) |
9 | | isofn 17476 |
. . . . . 6
⊢ (𝐶 ∈ Cat →
(Iso‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶))) |
10 | | fvex 6781 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
11 | | sqxpexg 7597 |
. . . . . . 7
⊢
((Base‘𝐶)
∈ V → ((Base‘𝐶) × (Base‘𝐶)) ∈ V) |
12 | 10, 11 | mp1i 13 |
. . . . . 6
⊢ (𝐶 ∈ Cat →
((Base‘𝐶) ×
(Base‘𝐶)) ∈
V) |
13 | | 0ex 5231 |
. . . . . . 7
⊢ ∅
∈ V |
14 | 13 | a1i 11 |
. . . . . 6
⊢ (𝐶 ∈ Cat → ∅
∈ V) |
15 | | suppvalfn 7974 |
. . . . . 6
⊢
(((Iso‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶)) ∧
((Base‘𝐶) ×
(Base‘𝐶)) ∈ V
∧ ∅ ∈ V) → ((Iso‘𝐶) supp ∅) = {𝑓 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∣ ((Iso‘𝐶)‘𝑓) ≠ ∅}) |
16 | 9, 12, 14, 15 | syl3anc 1370 |
. . . . 5
⊢ (𝐶 ∈ Cat →
((Iso‘𝐶) supp
∅) = {𝑓 ∈
((Base‘𝐶) ×
(Base‘𝐶)) ∣
((Iso‘𝐶)‘𝑓) ≠
∅}) |
17 | 16 | releqd 5685 |
. . . 4
⊢ (𝐶 ∈ Cat → (Rel
((Iso‘𝐶) supp
∅) ↔ Rel {𝑓
∈ ((Base‘𝐶)
× (Base‘𝐶))
∣ ((Iso‘𝐶)‘𝑓) ≠ ∅})) |
18 | 8, 17 | mpbird 256 |
. . 3
⊢ (𝐶 ∈ Cat → Rel
((Iso‘𝐶) supp
∅)) |
19 | | cicfval 17498 |
. . . 4
⊢ (𝐶 ∈ Cat → (
≃𝑐 ‘𝐶) = ((Iso‘𝐶) supp ∅)) |
20 | 19 | releqd 5685 |
. . 3
⊢ (𝐶 ∈ Cat → (Rel (
≃𝑐 ‘𝐶) ↔ Rel ((Iso‘𝐶) supp ∅))) |
21 | 18, 20 | mpbird 256 |
. 2
⊢ (𝐶 ∈ Cat → Rel (
≃𝑐 ‘𝐶)) |
22 | | cicsym 17505 |
. 2
⊢ ((𝐶 ∈ Cat ∧ 𝑥( ≃𝑐
‘𝐶)𝑦) → 𝑦( ≃𝑐 ‘𝐶)𝑥) |
23 | | cictr 17506 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ 𝑥( ≃𝑐
‘𝐶)𝑦 ∧ 𝑦( ≃𝑐 ‘𝐶)𝑧) → 𝑥( ≃𝑐 ‘𝐶)𝑧) |
24 | 23 | 3expb 1119 |
. 2
⊢ ((𝐶 ∈ Cat ∧ (𝑥( ≃𝑐
‘𝐶)𝑦 ∧ 𝑦( ≃𝑐 ‘𝐶)𝑧)) → 𝑥( ≃𝑐 ‘𝐶)𝑧) |
25 | | cicref 17502 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥( ≃𝑐 ‘𝐶)𝑥) |
26 | | ciclcl 17503 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ 𝑥( ≃𝑐
‘𝐶)𝑥) → 𝑥 ∈ (Base‘𝐶)) |
27 | 25, 26 | impbida 798 |
. 2
⊢ (𝐶 ∈ Cat → (𝑥 ∈ (Base‘𝐶) ↔ 𝑥( ≃𝑐 ‘𝐶)𝑥)) |
28 | 21, 22, 24, 27 | iserd 8513 |
1
⊢ (𝐶 ∈ Cat → (
≃𝑐 ‘𝐶) Er (Base‘𝐶)) |