Step | Hyp | Ref
| Expression |
1 | | bren 8636 |
. 2
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
2 | | bren 8636 |
. 2
⊢ (𝐶 ≈ 𝐷 ↔ ∃𝑔 𝑔:𝐶–1-1-onto→𝐷) |
3 | | exdistrv 1964 |
. . 3
⊢
(∃𝑓∃𝑔(𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ↔ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 ∧ ∃𝑔 𝑔:𝐶–1-1-onto→𝐷)) |
4 | | ovexd 7248 |
. . . . 5
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝐴 ↑m 𝐶) ∈ V) |
5 | | ovexd 7248 |
. . . . 5
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝐵 ↑m 𝐷) ∈ V) |
6 | | elmapi 8530 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ↑m 𝐶) → 𝑥:𝐶⟶𝐴) |
7 | | f1of 6661 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴⟶𝐵) |
8 | 7 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝑓:𝐴⟶𝐵) |
9 | | fco 6569 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥:𝐶⟶𝐴) → (𝑓 ∘ 𝑥):𝐶⟶𝐵) |
10 | 8, 9 | sylan 583 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐶⟶𝐴) → (𝑓 ∘ 𝑥):𝐶⟶𝐵) |
11 | | f1ocnv 6673 |
. . . . . . . . . . . 12
⊢ (𝑔:𝐶–1-1-onto→𝐷 → ◡𝑔:𝐷–1-1-onto→𝐶) |
12 | 11 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ◡𝑔:𝐷–1-1-onto→𝐶) |
13 | | f1of 6661 |
. . . . . . . . . . 11
⊢ (◡𝑔:𝐷–1-1-onto→𝐶 → ◡𝑔:𝐷⟶𝐶) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ◡𝑔:𝐷⟶𝐶) |
15 | 14 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐶⟶𝐴) → ◡𝑔:𝐷⟶𝐶) |
16 | 10, 15 | fcod 6571 |
. . . . . . . 8
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐶⟶𝐴) → ((𝑓 ∘ 𝑥) ∘ ◡𝑔):𝐷⟶𝐵) |
17 | 16 | ex 416 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝑥:𝐶⟶𝐴 → ((𝑓 ∘ 𝑥) ∘ ◡𝑔):𝐷⟶𝐵)) |
18 | 6, 17 | syl5 34 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝑥 ∈ (𝐴 ↑m 𝐶) → ((𝑓 ∘ 𝑥) ∘ ◡𝑔):𝐷⟶𝐵)) |
19 | | f1ofo 6668 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵) |
20 | 19 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝑓:𝐴–onto→𝐵) |
21 | | forn 6636 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵) |
22 | 20, 21 | syl 17 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ran 𝑓 = 𝐵) |
23 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
24 | 23 | rnex 7690 |
. . . . . . . 8
⊢ ran 𝑓 ∈ V |
25 | 22, 24 | eqeltrrdi 2847 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝐵 ∈ V) |
26 | | f1ofo 6668 |
. . . . . . . . . 10
⊢ (𝑔:𝐶–1-1-onto→𝐷 → 𝑔:𝐶–onto→𝐷) |
27 | 26 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝑔:𝐶–onto→𝐷) |
28 | | forn 6636 |
. . . . . . . . 9
⊢ (𝑔:𝐶–onto→𝐷 → ran 𝑔 = 𝐷) |
29 | 27, 28 | syl 17 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ran 𝑔 = 𝐷) |
30 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑔 ∈ V |
31 | 30 | rnex 7690 |
. . . . . . . 8
⊢ ran 𝑔 ∈ V |
32 | 29, 31 | eqeltrrdi 2847 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝐷 ∈ V) |
33 | 25, 32 | elmapd 8522 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∈ (𝐵 ↑m 𝐷) ↔ ((𝑓 ∘ 𝑥) ∘ ◡𝑔):𝐷⟶𝐵)) |
34 | 18, 33 | sylibrd 262 |
. . . . 5
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝑥 ∈ (𝐴 ↑m 𝐶) → ((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∈ (𝐵 ↑m 𝐷))) |
35 | | elmapi 8530 |
. . . . . . 7
⊢ (𝑦 ∈ (𝐵 ↑m 𝐷) → 𝑦:𝐷⟶𝐵) |
36 | | f1ocnv 6673 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–1-1-onto→𝐵 → ◡𝑓:𝐵–1-1-onto→𝐴) |
37 | 36 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ◡𝑓:𝐵–1-1-onto→𝐴) |
38 | | f1of 6661 |
. . . . . . . . . . 11
⊢ (◡𝑓:𝐵–1-1-onto→𝐴 → ◡𝑓:𝐵⟶𝐴) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ◡𝑓:𝐵⟶𝐴) |
40 | 39 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐷⟶𝐵) → ◡𝑓:𝐵⟶𝐴) |
41 | | id 22 |
. . . . . . . . . 10
⊢ (𝑦:𝐷⟶𝐵 → 𝑦:𝐷⟶𝐵) |
42 | | f1of 6661 |
. . . . . . . . . . 11
⊢ (𝑔:𝐶–1-1-onto→𝐷 → 𝑔:𝐶⟶𝐷) |
43 | 42 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝑔:𝐶⟶𝐷) |
44 | | fco 6569 |
. . . . . . . . . 10
⊢ ((𝑦:𝐷⟶𝐵 ∧ 𝑔:𝐶⟶𝐷) → (𝑦 ∘ 𝑔):𝐶⟶𝐵) |
45 | 41, 43, 44 | syl2anr 600 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐷⟶𝐵) → (𝑦 ∘ 𝑔):𝐶⟶𝐵) |
46 | 40, 45 | fcod 6571 |
. . . . . . . 8
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐷⟶𝐵) → (◡𝑓 ∘ (𝑦 ∘ 𝑔)):𝐶⟶𝐴) |
47 | 46 | ex 416 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝑦:𝐷⟶𝐵 → (◡𝑓 ∘ (𝑦 ∘ 𝑔)):𝐶⟶𝐴)) |
48 | 35, 47 | syl5 34 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝑦 ∈ (𝐵 ↑m 𝐷) → (◡𝑓 ∘ (𝑦 ∘ 𝑔)):𝐶⟶𝐴)) |
49 | | f1odm 6665 |
. . . . . . . . 9
⊢ (𝑓:𝐴–1-1-onto→𝐵 → dom 𝑓 = 𝐴) |
50 | 49 | adantr 484 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → dom 𝑓 = 𝐴) |
51 | 23 | dmex 7689 |
. . . . . . . 8
⊢ dom 𝑓 ∈ V |
52 | 50, 51 | eqeltrrdi 2847 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝐴 ∈ V) |
53 | | f1odm 6665 |
. . . . . . . . 9
⊢ (𝑔:𝐶–1-1-onto→𝐷 → dom 𝑔 = 𝐶) |
54 | 53 | adantl 485 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → dom 𝑔 = 𝐶) |
55 | 30 | dmex 7689 |
. . . . . . . 8
⊢ dom 𝑔 ∈ V |
56 | 54, 55 | eqeltrrdi 2847 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → 𝐶 ∈ V) |
57 | 52, 56 | elmapd 8522 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ((◡𝑓 ∘ (𝑦 ∘ 𝑔)) ∈ (𝐴 ↑m 𝐶) ↔ (◡𝑓 ∘ (𝑦 ∘ 𝑔)):𝐶⟶𝐴)) |
58 | 48, 57 | sylibrd 262 |
. . . . 5
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝑦 ∈ (𝐵 ↑m 𝐷) → (◡𝑓 ∘ (𝑦 ∘ 𝑔)) ∈ (𝐴 ↑m 𝐶))) |
59 | | coass 6129 |
. . . . . . . . . . 11
⊢ ((𝑓 ∘ ◡𝑓) ∘ (𝑦 ∘ 𝑔)) = (𝑓 ∘ (◡𝑓 ∘ (𝑦 ∘ 𝑔))) |
60 | | f1ococnv2 6687 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝑓 ∘ ◡𝑓) = ( I ↾ 𝐵)) |
61 | 60 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (𝑓 ∘ ◡𝑓) = ( I ↾ 𝐵)) |
62 | 61 | coeq1d 5730 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ ◡𝑓) ∘ (𝑦 ∘ 𝑔)) = (( I ↾ 𝐵) ∘ (𝑦 ∘ 𝑔))) |
63 | 45 | adantrl 716 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (𝑦 ∘ 𝑔):𝐶⟶𝐵) |
64 | | fcoi2 6594 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∘ 𝑔):𝐶⟶𝐵 → (( I ↾ 𝐵) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (( I ↾ 𝐵) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔)) |
66 | 62, 65 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ ◡𝑓) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔)) |
67 | 59, 66 | eqtr3id 2792 |
. . . . . . . . . 10
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (𝑓 ∘ (◡𝑓 ∘ (𝑦 ∘ 𝑔))) = (𝑦 ∘ 𝑔)) |
68 | 67 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) = (𝑓 ∘ (◡𝑓 ∘ (𝑦 ∘ 𝑔))) ↔ (𝑓 ∘ 𝑥) = (𝑦 ∘ 𝑔))) |
69 | | coass 6129 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = ((𝑓 ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) |
70 | | f1ococnv1 6689 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:𝐶–1-1-onto→𝐷 → (◡𝑔 ∘ 𝑔) = ( I ↾ 𝐶)) |
71 | 70 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (◡𝑔 ∘ 𝑔) = ( I ↾ 𝐶)) |
72 | 71 | coeq2d 5731 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) = ((𝑓 ∘ 𝑥) ∘ ( I ↾ 𝐶))) |
73 | 10 | adantrr 717 |
. . . . . . . . . . . . . 14
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (𝑓 ∘ 𝑥):𝐶⟶𝐵) |
74 | | fcoi1 6593 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∘ 𝑥):𝐶⟶𝐵 → ((𝑓 ∘ 𝑥) ∘ ( I ↾ 𝐶)) = (𝑓 ∘ 𝑥)) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) ∘ ( I ↾ 𝐶)) = (𝑓 ∘ 𝑥)) |
76 | 72, 75 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) = (𝑓 ∘ 𝑥)) |
77 | 69, 76 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = (𝑓 ∘ 𝑥)) |
78 | 77 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑦 ∘ 𝑔) = (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ (𝑦 ∘ 𝑔) = (𝑓 ∘ 𝑥))) |
79 | | eqcom 2744 |
. . . . . . . . . 10
⊢ ((𝑦 ∘ 𝑔) = (𝑓 ∘ 𝑥) ↔ (𝑓 ∘ 𝑥) = (𝑦 ∘ 𝑔)) |
80 | 78, 79 | bitrdi 290 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑦 ∘ 𝑔) = (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ (𝑓 ∘ 𝑥) = (𝑦 ∘ 𝑔))) |
81 | 68, 80 | bitr4d 285 |
. . . . . . . 8
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) = (𝑓 ∘ (◡𝑓 ∘ (𝑦 ∘ 𝑔))) ↔ (𝑦 ∘ 𝑔) = (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔))) |
82 | | f1of1 6660 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–1-1→𝐵) |
83 | 82 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → 𝑓:𝐴–1-1→𝐵) |
84 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → 𝑥:𝐶⟶𝐴) |
85 | 46 | adantrl 716 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (◡𝑓 ∘ (𝑦 ∘ 𝑔)):𝐶⟶𝐴) |
86 | | cocan1 7101 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑥:𝐶⟶𝐴 ∧ (◡𝑓 ∘ (𝑦 ∘ 𝑔)):𝐶⟶𝐴) → ((𝑓 ∘ 𝑥) = (𝑓 ∘ (◡𝑓 ∘ (𝑦 ∘ 𝑔))) ↔ 𝑥 = (◡𝑓 ∘ (𝑦 ∘ 𝑔)))) |
87 | 83, 84, 85, 86 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) = (𝑓 ∘ (◡𝑓 ∘ (𝑦 ∘ 𝑔))) ↔ 𝑥 = (◡𝑓 ∘ (𝑦 ∘ 𝑔)))) |
88 | 27 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → 𝑔:𝐶–onto→𝐷) |
89 | | ffn 6545 |
. . . . . . . . . 10
⊢ (𝑦:𝐷⟶𝐵 → 𝑦 Fn 𝐷) |
90 | 89 | ad2antll 729 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → 𝑦 Fn 𝐷) |
91 | 16 | adantrr 717 |
. . . . . . . . . 10
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) ∘ ◡𝑔):𝐷⟶𝐵) |
92 | 91 | ffnd 6546 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑓 ∘ 𝑥) ∘ ◡𝑔) Fn 𝐷) |
93 | | cocan2 7102 |
. . . . . . . . 9
⊢ ((𝑔:𝐶–onto→𝐷 ∧ 𝑦 Fn 𝐷 ∧ ((𝑓 ∘ 𝑥) ∘ ◡𝑔) Fn 𝐷) → ((𝑦 ∘ 𝑔) = (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ 𝑦 = ((𝑓 ∘ 𝑥) ∘ ◡𝑔))) |
94 | 88, 90, 92, 93 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → ((𝑦 ∘ 𝑔) = (((𝑓 ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ 𝑦 = ((𝑓 ∘ 𝑥) ∘ ◡𝑔))) |
95 | 81, 87, 94 | 3bitr3d 312 |
. . . . . . 7
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵)) → (𝑥 = (◡𝑓 ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((𝑓 ∘ 𝑥) ∘ ◡𝑔))) |
96 | 95 | ex 416 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ((𝑥:𝐶⟶𝐴 ∧ 𝑦:𝐷⟶𝐵) → (𝑥 = (◡𝑓 ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((𝑓 ∘ 𝑥) ∘ ◡𝑔)))) |
97 | 6, 35, 96 | syl2ani 610 |
. . . . 5
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → ((𝑥 ∈ (𝐴 ↑m 𝐶) ∧ 𝑦 ∈ (𝐵 ↑m 𝐷)) → (𝑥 = (◡𝑓 ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((𝑓 ∘ 𝑥) ∘ ◡𝑔)))) |
98 | 4, 5, 34, 58, 97 | en3d 8665 |
. . . 4
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝐴 ↑m 𝐶) ≈ (𝐵 ↑m 𝐷)) |
99 | 98 | exlimivv 1940 |
. . 3
⊢
(∃𝑓∃𝑔(𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐶–1-1-onto→𝐷) → (𝐴 ↑m 𝐶) ≈ (𝐵 ↑m 𝐷)) |
100 | 3, 99 | sylbir 238 |
. 2
⊢
((∃𝑓 𝑓:𝐴–1-1-onto→𝐵 ∧ ∃𝑔 𝑔:𝐶–1-1-onto→𝐷) → (𝐴 ↑m 𝐶) ≈ (𝐵 ↑m 𝐷)) |
101 | 1, 2, 100 | syl2anb 601 |
1
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ↑m 𝐶) ≈ (𝐵 ↑m 𝐷)) |