Step | Hyp | Ref
| Expression |
1 | | bren 8512 |
. 2
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
2 | | bren 8512 |
. 2
⊢ (𝐶 ≈ 𝐷 ↔ ∃𝑔 𝑔:𝐶–1-1-onto→𝐷) |
3 | | exdistrv 1952 |
. . 3
⊢
(∃𝑓∃𝑔(𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ↔ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 ∧ ∃𝑔 𝑔:𝐶–1-1-onto→𝐷)) |
4 | | ovexd 7185 |
. . . . 5
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝐴 ↑m 𝐶) ∈ V) |
5 | | ovexd 7185 |
. . . . 5
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝐵 ↑m 𝐷) ∈ V) |
6 | | elmapi 8422 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ↑m 𝐶) → 𝑥:𝐶⟶𝐴) |
7 | | f1of 6610 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴⟶𝐵) |
8 | 7 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝑓:𝐴⟶𝐵) |
9 | | fco 6526 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥:𝐶⟶𝐴) → (𝑓 ∘ 𝑥):𝐶⟶𝐵) |
10 | 8, 9 | sylan 582 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐶⟶𝐴) → (𝑓 ∘ 𝑥):𝐶⟶𝐵) |
11 | | f1ocnv 6622 |
. . . . . . . . . . . 12
⊢ (𝑔:𝐶–1-1-onto→𝐷 → ◡𝑔:𝐷–1-1-onto→𝐶) |
12 | 11 | adantl 484 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ◡𝑔:𝐷–1-1-onto→𝐶) |
13 | | f1of 6610 |
. . . . . . . . . . 11
⊢ (◡𝑔:𝐷–1-1-onto→𝐶 → ◡𝑔:𝐷⟶𝐶) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ◡𝑔:𝐷⟶𝐶) |
15 | 14 | adantr 483 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐶⟶𝐴) → ◡𝑔:𝐷⟶𝐶) |
16 | | fco 6526 |
. . . . . . . . 9
⊢ (((𝑓 ∘ 𝑥):𝐶⟶𝐵 ∧ ◡𝑔:𝐷⟶𝐶) → ((𝑓 ∘ 𝑥) ∘ ◡𝑔):𝐷⟶𝐵) |
17 | 10, 15, 16 | syl2anc 586 |
. . . . . . . 8
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐶⟶𝐴) → ((𝑓 ∘ 𝑥) ∘ ◡𝑔):𝐷⟶𝐵) |
18 | 17 | ex 415 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝑥:𝐶⟶𝐴 → ((𝑓 ∘ 𝑥) ∘ ◡𝑔):𝐷⟶𝐵)) |
19 | 6, 18 | syl5 34 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝑥 ∈ (𝐴 ↑m 𝐶) → ((𝑓 ∘ 𝑥) ∘ ◡𝑔):𝐷⟶𝐵)) |
20 | | f1ofo 6617 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵) |
21 | 20 | adantr 483 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝑓:𝐴–onto→𝐵) |
22 | | forn 6588 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ran 𝑓 = 𝐵) |
24 | | vex 3498 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
25 | 24 | rnex 7611 |
. . . . . . . 8
⊢ ran 𝑓 ∈ V |
26 | 23, 25 | eqeltrrdi 2922 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝐵 ∈ V) |
27 | | f1ofo 6617 |
. . . . . . . . . 10
⊢ (𝑔:𝐶–1-1-onto→𝐷 → 𝑔:𝐶–onto→𝐷) |
28 | 27 | adantl 484 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝑔:𝐶–onto→𝐷) |
29 | | forn 6588 |
. . . . . . . . 9
⊢ (𝑔:𝐶–onto→𝐷 → ran 𝑔 = 𝐷) |
30 | 28, 29 | syl 17 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ran 𝑔 = 𝐷) |
31 | | vex 3498 |
. . . . . . . . 9
⊢ 𝑔 ∈ V |
32 | 31 | rnex 7611 |
. . . . . . . 8
⊢ ran 𝑔 ∈ V |
33 | 30, 32 | eqeltrrdi 2922 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝐷 ∈ V) |
34 | 26, 33 | elmapd 8414 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∈ (𝐵 ↑m 𝐷) ↔ ((𝑓 ∘ 𝑥) ∘ ◡𝑔):𝐷⟶𝐵)) |
35 | 19, 34 | sylibrd 261 |
. . . . 5
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝑥 ∈ (𝐴 ↑m 𝐶) → ((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∈ (𝐵 ↑m 𝐷))) |
36 | | elmapi 8422 |
. . . . . . 7
⊢ (𝑦 ∈ (𝐵 ↑m 𝐷) → 𝑦:𝐷⟶𝐵) |
37 | | f1ocnv 6622 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–1-1-onto→𝐵 → ◡𝑓:𝐵–1-1-onto→𝐴) |
38 | 37 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ◡𝑓:𝐵–1-1-onto→𝐴) |
39 | | f1of 6610 |
. . . . . . . . . . 11
⊢ (◡𝑓:𝐵–1-1-onto→𝐴 → ◡𝑓:𝐵⟶𝐴) |
40 | 38, 39 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ◡𝑓:𝐵⟶𝐴) |
41 | 40 | adantr 483 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐷⟶𝐵) → ◡𝑓:𝐵⟶𝐴) |
42 | | id 22 |
. . . . . . . . . 10
⊢ (𝑦:𝐷⟶𝐵 → 𝑦:𝐷⟶𝐵) |
43 | | f1of 6610 |
. . . . . . . . . . 11
⊢ (𝑔:𝐶–1-1-onto→𝐷 → 𝑔:𝐶⟶𝐷) |
44 | 43 | adantl 484 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝑔:𝐶⟶𝐷) |
45 | | fco 6526 |
. . . . . . . . . 10
⊢ ((𝑦:𝐷⟶𝐵 ∧ 𝑔:𝐶⟶𝐷) → (𝑦 ∘ 𝑔):𝐶⟶𝐵) |
46 | 42, 44, 45 | syl2anr 598 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐷⟶𝐵) → (𝑦 ∘ 𝑔):𝐶⟶𝐵) |
47 | | fco 6526 |
. . . . . . . . 9
⊢ ((◡𝑓:𝐵⟶𝐴 ∧ (𝑦 ∘ 𝑔):𝐶⟶𝐵) → (◡𝑓 ∘ (𝑦 ∘ 𝑔)):𝐶⟶𝐴) |
48 | 41, 46, 47 | syl2anc 586 |
. . . . . . . 8
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐷⟶𝐵) → (◡𝑓 ∘ (𝑦 ∘ 𝑔)):𝐶⟶𝐴) |
49 | 48 | ex 415 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝑦:𝐷⟶𝐵 → (◡𝑓 ∘ (𝑦 ∘ 𝑔)):𝐶⟶𝐴)) |
50 | 36, 49 | syl5 34 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝑦 ∈ (𝐵 ↑m 𝐷) → (◡𝑓 ∘ (𝑦 ∘ 𝑔)):𝐶⟶𝐴)) |
51 | | f1odm 6614 |
. . . . . . . . 9
⊢ (𝑓:𝐴–1-1-onto→𝐵 → dom 𝑓 = 𝐴) |
52 | 51 | adantr 483 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → dom 𝑓 = 𝐴) |
53 | 24 | dmex 7610 |
. . . . . . . 8
⊢ dom 𝑓 ∈ V |
54 | 52, 53 | eqeltrrdi 2922 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝐴 ∈ V) |
55 | | f1odm 6614 |
. . . . . . . . 9
⊢ (𝑔:𝐶–1-1-onto→𝐷 → dom 𝑔 = 𝐶) |
56 | 55 | adantl 484 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → dom 𝑔 = 𝐶) |
57 | 31 | dmex 7610 |
. . . . . . . 8
⊢ dom 𝑔 ∈ V |
58 | 56, 57 | eqeltrrdi 2922 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝐶 ∈ V) |
59 | 54, 58 | elmapd 8414 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ((◡𝑓 ∘ (𝑦 ∘ 𝑔)) ∈ (𝐴 ↑m 𝐶) ↔ (◡𝑓 ∘ (𝑦 ∘ 𝑔)):𝐶⟶𝐴)) |
60 | 50, 59 | sylibrd 261 |
. . . . 5
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝑦 ∈ (𝐵 ↑m 𝐷) → (◡𝑓 ∘ (𝑦 ∘ 𝑔)) ∈ (𝐴 ↑m 𝐶))) |
61 | | coass 6113 |
. . . . . . . . . . 11
⊢ ((𝑓 ∘ ◡𝑓) ∘ (𝑦 ∘ 𝑔)) = (𝑓 ∘ (◡𝑓 ∘ (𝑦 ∘ 𝑔))) |
62 | | f1ococnv2 6636 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝑓 ∘ ◡𝑓) = ( I ↾ 𝐵)) |
63 | 62 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (𝑓 ∘ ◡𝑓) = ( I ↾ 𝐵)) |
64 | 63 | coeq1d 5727 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ ◡𝑓) ∘ (𝑦 ∘ 𝑔)) = (( I ↾ 𝐵) ∘ (𝑦 ∘ 𝑔))) |
65 | 46 | adantrl 714 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (𝑦 ∘ 𝑔):𝐶⟶𝐵) |
66 | | fcoi2 6548 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∘ 𝑔):𝐶⟶𝐵 → (( I ↾ 𝐵) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (( I ↾ 𝐵) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔)) |
68 | 64, 67 | eqtrd 2856 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ ◡𝑓) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔)) |
69 | 61, 68 | syl5eqr 2870 |
. . . . . . . . . 10
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (𝑓 ∘ (◡𝑓 ∘ (𝑦 ∘ 𝑔))) = (𝑦 ∘ 𝑔)) |
70 | 69 | eqeq2d 2832 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) = (𝑓 ∘ (◡𝑓 ∘ (𝑦 ∘ 𝑔))) ↔ (𝑓 ∘ 𝑥) = (𝑦 ∘ 𝑔))) |
71 | | coass 6113 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = ((𝑓 ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) |
72 | | f1ococnv1 6638 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:𝐶–1-1-onto→𝐷 → (◡𝑔 ∘ 𝑔) = ( I ↾ 𝐶)) |
73 | 72 | ad2antlr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (◡𝑔 ∘ 𝑔) = ( I ↾ 𝐶)) |
74 | 73 | coeq2d 5728 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) = ((𝑓 ∘ 𝑥) ∘ ( I ↾ 𝐶))) |
75 | 10 | adantrr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (𝑓 ∘ 𝑥):𝐶⟶𝐵) |
76 | | fcoi1 6547 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∘ 𝑥):𝐶⟶𝐵 → ((𝑓 ∘ 𝑥) ∘ ( I ↾ 𝐶)) = (𝑓 ∘ 𝑥)) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) ∘ ( I ↾ 𝐶)) = (𝑓 ∘ 𝑥)) |
78 | 74, 77 | eqtrd 2856 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) = (𝑓 ∘ 𝑥)) |
79 | 71, 78 | syl5eq 2868 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = (𝑓 ∘ 𝑥)) |
80 | 79 | eqeq2d 2832 |
. . . . . . . . . 10
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑦 ∘ 𝑔) = (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ (𝑦 ∘ 𝑔) = (𝑓 ∘ 𝑥))) |
81 | | eqcom 2828 |
. . . . . . . . . 10
⊢ ((𝑦 ∘ 𝑔) = (𝑓 ∘ 𝑥) ↔ (𝑓 ∘ 𝑥) = (𝑦 ∘ 𝑔)) |
82 | 80, 81 | syl6bb 289 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑦 ∘ 𝑔) = (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ (𝑓 ∘ 𝑥) = (𝑦 ∘ 𝑔))) |
83 | 70, 82 | bitr4d 284 |
. . . . . . . 8
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) = (𝑓 ∘ (◡𝑓 ∘ (𝑦 ∘ 𝑔))) ↔ (𝑦 ∘ 𝑔) = (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔))) |
84 | | f1of1 6609 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–1-1→𝐵) |
85 | 84 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → 𝑓:𝐴–1-1→𝐵) |
86 | | simprl 769 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → 𝑥:𝐶⟶𝐴) |
87 | 48 | adantrl 714 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (◡𝑓 ∘ (𝑦 ∘ 𝑔)):𝐶⟶𝐴) |
88 | | cocan1 7041 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑥:𝐶⟶𝐴 ∧ (◡𝑓 ∘ (𝑦 ∘ 𝑔)):𝐶⟶𝐴) → ((𝑓 ∘ 𝑥) = (𝑓 ∘ (◡𝑓 ∘ (𝑦 ∘ 𝑔))) ↔ 𝑥 = (◡𝑓 ∘ (𝑦 ∘ 𝑔)))) |
89 | 85, 86, 87, 88 | syl3anc 1367 |
. . . . . . . 8
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) = (𝑓 ∘ (◡𝑓 ∘ (𝑦 ∘ 𝑔))) ↔ 𝑥 = (◡𝑓 ∘ (𝑦 ∘ 𝑔)))) |
90 | 28 | adantr 483 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → 𝑔:𝐶–onto→𝐷) |
91 | | ffn 6509 |
. . . . . . . . . 10
⊢ (𝑦:𝐷⟶𝐵 → 𝑦 Fn 𝐷) |
92 | 91 | ad2antll 727 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → 𝑦 Fn 𝐷) |
93 | 17 | adantrr 715 |
. . . . . . . . . 10
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) ∘ ◡𝑔):𝐷⟶𝐵) |
94 | 93 | ffnd 6510 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) ∘ ◡𝑔) Fn 𝐷) |
95 | | cocan2 7042 |
. . . . . . . . 9
⊢ ((𝑔:𝐶–onto→𝐷 ∧ 𝑦 Fn 𝐷 ∧ ((𝑓 ∘ 𝑥) ∘ ◡𝑔) Fn 𝐷) → ((𝑦 ∘ 𝑔) = (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ 𝑦 = ((𝑓 ∘ 𝑥) ∘ ◡𝑔))) |
96 | 90, 92, 94, 95 | syl3anc 1367 |
. . . . . . . 8
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑦 ∘ 𝑔) = (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ 𝑦 = ((𝑓 ∘ 𝑥) ∘ ◡𝑔))) |
97 | 83, 89, 96 | 3bitr3d 311 |
. . . . . . 7
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (𝑥 = (◡𝑓 ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((𝑓 ∘ 𝑥) ∘ ◡𝑔))) |
98 | 97 | ex 415 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ((𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵) → (𝑥 = (◡𝑓 ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((𝑓 ∘ 𝑥) ∘ ◡𝑔)))) |
99 | 6, 36, 98 | syl2ani 608 |
. . . . 5
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ((𝑥 ∈ (𝐴 ↑m 𝐶) ∧ 𝑦 ∈ (𝐵 ↑m 𝐷)) → (𝑥 = (◡𝑓 ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((𝑓 ∘ 𝑥) ∘ ◡𝑔)))) |
100 | 4, 5, 35, 60, 99 | en3d 8540 |
. . . 4
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝐴 ↑m 𝐶) ≈ (𝐵 ↑m 𝐷)) |
101 | 100 | exlimivv 1929 |
. . 3
⊢
(∃𝑓∃𝑔(𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝐴 ↑m 𝐶) ≈ (𝐵 ↑m 𝐷)) |
102 | 3, 101 | sylbir 237 |
. 2
⊢
((∃𝑓 𝑓:𝐴–1-1-onto→𝐵 ∧ ∃𝑔 𝑔:𝐶–1-1-onto→𝐷) → (𝐴 ↑m 𝐶) ≈ (𝐵 ↑m 𝐷)) |
103 | 1, 2, 102 | syl2anb 599 |
1
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ↑m 𝐶) ≈ (𝐵 ↑m 𝐷)) |