Proof of Theorem brcic
Step | Hyp | Ref
| Expression |
1 | | cic.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
2 | | cicfval 16280 |
. . . 4
⊢ (𝐶 ∈ Cat → (
≃𝑐 ‘𝐶) = ((Iso‘𝐶) supp ∅)) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → (
≃𝑐 ‘𝐶) = ((Iso‘𝐶) supp ∅)) |
4 | 3 | breqd 4594 |
. 2
⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ 𝑋((Iso‘𝐶) supp ∅)𝑌)) |
5 | | df-br 4584 |
. . 3
⊢ (𝑋((Iso‘𝐶) supp ∅)𝑌 ↔ 〈𝑋, 𝑌〉 ∈ ((Iso‘𝐶) supp ∅)) |
6 | 5 | a1i 11 |
. 2
⊢ (𝜑 → (𝑋((Iso‘𝐶) supp ∅)𝑌 ↔ 〈𝑋, 𝑌〉 ∈ ((Iso‘𝐶) supp ∅))) |
7 | | cic.i |
. . . . . 6
⊢ 𝐼 = (Iso‘𝐶) |
8 | 7 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐼 = (Iso‘𝐶)) |
9 | 8 | fveq1d 6105 |
. . . 4
⊢ (𝜑 → (𝐼‘〈𝑋, 𝑌〉) = ((Iso‘𝐶)‘〈𝑋, 𝑌〉)) |
10 | 9 | neeq1d 2841 |
. . 3
⊢ (𝜑 → ((𝐼‘〈𝑋, 𝑌〉) ≠ ∅ ↔
((Iso‘𝐶)‘〈𝑋, 𝑌〉) ≠ ∅)) |
11 | | df-ov 6552 |
. . . . . 6
⊢ (𝑋𝐼𝑌) = (𝐼‘〈𝑋, 𝑌〉) |
12 | 11 | eqcomi 2619 |
. . . . 5
⊢ (𝐼‘〈𝑋, 𝑌〉) = (𝑋𝐼𝑌) |
13 | 12 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐼‘〈𝑋, 𝑌〉) = (𝑋𝐼𝑌)) |
14 | 13 | neeq1d 2841 |
. . 3
⊢ (𝜑 → ((𝐼‘〈𝑋, 𝑌〉) ≠ ∅ ↔ (𝑋𝐼𝑌) ≠ ∅)) |
15 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝐶)
∈ V |
16 | 15 | a1i 11 |
. . . . 5
⊢ (𝜑 → (Base‘𝐶) ∈ V) |
17 | | sqxpexg 6861 |
. . . . 5
⊢
((Base‘𝐶)
∈ V → ((Base‘𝐶) × (Base‘𝐶)) ∈ V) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ (𝜑 → ((Base‘𝐶) × (Base‘𝐶)) ∈ V) |
19 | | cic.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
20 | | cic.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
21 | 19, 20 | syl6eleq 2698 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) |
22 | | cic.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
23 | 22, 20 | syl6eleq 2698 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) |
24 | | opelxp 5070 |
. . . . 5
⊢
(〈𝑋, 𝑌〉 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↔ (𝑋 ∈ (Base‘𝐶) ∧ 𝑌 ∈ (Base‘𝐶))) |
25 | 21, 23, 24 | sylanbrc 695 |
. . . 4
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
26 | | isofn 16258 |
. . . . 5
⊢ (𝐶 ∈ Cat →
(Iso‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶))) |
27 | 1, 26 | syl 17 |
. . . 4
⊢ (𝜑 → (Iso‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))) |
28 | | fvn0elsuppb 7199 |
. . . 4
⊢
((((Base‘𝐶)
× (Base‘𝐶))
∈ V ∧ 〈𝑋,
𝑌〉 ∈
((Base‘𝐶) ×
(Base‘𝐶)) ∧
(Iso‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶))) →
(((Iso‘𝐶)‘〈𝑋, 𝑌〉) ≠ ∅ ↔ 〈𝑋, 𝑌〉 ∈ ((Iso‘𝐶) supp ∅))) |
29 | 18, 25, 27, 28 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (((Iso‘𝐶)‘〈𝑋, 𝑌〉) ≠ ∅ ↔ 〈𝑋, 𝑌〉 ∈ ((Iso‘𝐶) supp ∅))) |
30 | 10, 14, 29 | 3bitr3rd 298 |
. 2
⊢ (𝜑 → (〈𝑋, 𝑌〉 ∈ ((Iso‘𝐶) supp ∅) ↔ (𝑋𝐼𝑌) ≠ ∅)) |
31 | 4, 6, 30 | 3bitrd 293 |
1
⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ (𝑋𝐼𝑌) ≠ ∅)) |