Step | Hyp | Ref
| Expression |
1 | | cicrcl 17511 |
. 2
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐
‘𝐶)𝑆) → 𝑆 ∈ (Base‘𝐶)) |
2 | | ciclcl 17510 |
. 2
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐
‘𝐶)𝑆) → 𝑅 ∈ (Base‘𝐶)) |
3 | | eqid 2740 |
. . . . 5
⊢
(Iso‘𝐶) =
(Iso‘𝐶) |
4 | | eqid 2740 |
. . . . 5
⊢
(Base‘𝐶) =
(Base‘𝐶) |
5 | | simpl 483 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat) |
6 | | simpr 485 |
. . . . . 6
⊢ ((𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶)) → 𝑅 ∈ (Base‘𝐶)) |
7 | 6 | adantl 482 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → 𝑅 ∈ (Base‘𝐶)) |
8 | | simpl 483 |
. . . . . 6
⊢ ((𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶)) → 𝑆 ∈ (Base‘𝐶)) |
9 | 8 | adantl 482 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → 𝑆 ∈ (Base‘𝐶)) |
10 | 3, 4, 5, 7, 9 | cic 17507 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑅( ≃𝑐 ‘𝐶)𝑆 ↔ ∃𝑓 𝑓 ∈ (𝑅(Iso‘𝐶)𝑆))) |
11 | | eqid 2740 |
. . . . . . . . . 10
⊢
(Inv‘𝐶) =
(Inv‘𝐶) |
12 | 4, 11, 5, 7, 9, 3 | isoval 17473 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑅(Iso‘𝐶)𝑆) = dom (𝑅(Inv‘𝐶)𝑆)) |
13 | 4, 11, 5, 9, 7 | invsym2 17471 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → ◡(𝑆(Inv‘𝐶)𝑅) = (𝑅(Inv‘𝐶)𝑆)) |
14 | 13 | eqcomd 2746 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑅(Inv‘𝐶)𝑆) = ◡(𝑆(Inv‘𝐶)𝑅)) |
15 | 14 | dmeqd 5812 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → dom (𝑅(Inv‘𝐶)𝑆) = dom ◡(𝑆(Inv‘𝐶)𝑅)) |
16 | | df-rn 5600 |
. . . . . . . . . 10
⊢ ran
(𝑆(Inv‘𝐶)𝑅) = dom ◡(𝑆(Inv‘𝐶)𝑅) |
17 | 15, 16 | eqtr4di 2798 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → dom (𝑅(Inv‘𝐶)𝑆) = ran (𝑆(Inv‘𝐶)𝑅)) |
18 | 12, 17 | eqtrd 2780 |
. . . . . . . 8
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑅(Iso‘𝐶)𝑆) = ran (𝑆(Inv‘𝐶)𝑅)) |
19 | 18 | eleq2d 2826 |
. . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑓 ∈ (𝑅(Iso‘𝐶)𝑆) ↔ 𝑓 ∈ ran (𝑆(Inv‘𝐶)𝑅))) |
20 | | vex 3435 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
21 | | elrng 5798 |
. . . . . . . 8
⊢ (𝑓 ∈ V → (𝑓 ∈ ran (𝑆(Inv‘𝐶)𝑅) ↔ ∃𝑔 𝑔(𝑆(Inv‘𝐶)𝑅)𝑓)) |
22 | 20, 21 | mp1i 13 |
. . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑓 ∈ ran (𝑆(Inv‘𝐶)𝑅) ↔ ∃𝑔 𝑔(𝑆(Inv‘𝐶)𝑅)𝑓)) |
23 | 19, 22 | bitrd 278 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑓 ∈ (𝑅(Iso‘𝐶)𝑆) ↔ ∃𝑔 𝑔(𝑆(Inv‘𝐶)𝑅)𝑓)) |
24 | | df-br 5080 |
. . . . . . . 8
⊢ (𝑔(𝑆(Inv‘𝐶)𝑅)𝑓 ↔ 〈𝑔, 𝑓〉 ∈ (𝑆(Inv‘𝐶)𝑅)) |
25 | 24 | exbii 1854 |
. . . . . . 7
⊢
(∃𝑔 𝑔(𝑆(Inv‘𝐶)𝑅)𝑓 ↔ ∃𝑔〈𝑔, 𝑓〉 ∈ (𝑆(Inv‘𝐶)𝑅)) |
26 | | vex 3435 |
. . . . . . . . . . 11
⊢ 𝑔 ∈ V |
27 | 26, 20 | opeldm 5814 |
. . . . . . . . . 10
⊢
(〈𝑔, 𝑓〉 ∈ (𝑆(Inv‘𝐶)𝑅) → 𝑔 ∈ dom (𝑆(Inv‘𝐶)𝑅)) |
28 | 4, 11, 5, 9, 7, 3 | isoval 17473 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑆(Iso‘𝐶)𝑅) = dom (𝑆(Inv‘𝐶)𝑅)) |
29 | 28 | eqcomd 2746 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → dom (𝑆(Inv‘𝐶)𝑅) = (𝑆(Iso‘𝐶)𝑅)) |
30 | 29 | eleq2d 2826 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑔 ∈ dom (𝑆(Inv‘𝐶)𝑅) ↔ 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅))) |
31 | 5 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅)) → 𝐶 ∈ Cat) |
32 | 9 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅)) → 𝑆 ∈ (Base‘𝐶)) |
33 | 7 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅)) → 𝑅 ∈ (Base‘𝐶)) |
34 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅)) → 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅)) |
35 | 3, 4, 31, 32, 33, 34 | brcici 17508 |
. . . . . . . . . . . 12
⊢ (((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅)) → 𝑆( ≃𝑐 ‘𝐶)𝑅) |
36 | 35 | ex 413 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑔 ∈ (𝑆(Iso‘𝐶)𝑅) → 𝑆( ≃𝑐 ‘𝐶)𝑅)) |
37 | 30, 36 | sylbid 239 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑔 ∈ dom (𝑆(Inv‘𝐶)𝑅) → 𝑆( ≃𝑐 ‘𝐶)𝑅)) |
38 | 27, 37 | syl5com 31 |
. . . . . . . . 9
⊢
(〈𝑔, 𝑓〉 ∈ (𝑆(Inv‘𝐶)𝑅) → ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → 𝑆( ≃𝑐 ‘𝐶)𝑅)) |
39 | 38 | exlimiv 1937 |
. . . . . . . 8
⊢
(∃𝑔〈𝑔, 𝑓〉 ∈ (𝑆(Inv‘𝐶)𝑅) → ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → 𝑆( ≃𝑐 ‘𝐶)𝑅)) |
40 | 39 | com12 32 |
. . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (∃𝑔〈𝑔, 𝑓〉 ∈ (𝑆(Inv‘𝐶)𝑅) → 𝑆( ≃𝑐 ‘𝐶)𝑅)) |
41 | 25, 40 | syl5bi 241 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (∃𝑔 𝑔(𝑆(Inv‘𝐶)𝑅)𝑓 → 𝑆( ≃𝑐 ‘𝐶)𝑅)) |
42 | 23, 41 | sylbid 239 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑓 ∈ (𝑅(Iso‘𝐶)𝑆) → 𝑆( ≃𝑐 ‘𝐶)𝑅)) |
43 | 42 | exlimdv 1940 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (∃𝑓 𝑓 ∈ (𝑅(Iso‘𝐶)𝑆) → 𝑆( ≃𝑐 ‘𝐶)𝑅)) |
44 | 10, 43 | sylbid 239 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑅( ≃𝑐 ‘𝐶)𝑆 → 𝑆( ≃𝑐 ‘𝐶)𝑅)) |
45 | 44 | impancom 452 |
. 2
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐
‘𝐶)𝑆) → ((𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶)) → 𝑆( ≃𝑐 ‘𝐶)𝑅)) |
46 | 1, 2, 45 | mp2and 696 |
1
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐
‘𝐶)𝑆) → 𝑆( ≃𝑐 ‘𝐶)𝑅) |