Step | Hyp | Ref
| Expression |
1 | | bren 8564 |
. 2
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑔 𝑔:𝐴–1-1-onto→𝐵) |
2 | | bren 8564 |
. 2
⊢ (𝐶 ≈ 𝐷 ↔ ∃ℎ ℎ:𝐶–1-1-onto→𝐷) |
3 | | exdistrv 1963 |
. . 3
⊢
(∃𝑔∃ℎ(𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ↔ (∃𝑔 𝑔:𝐴–1-1-onto→𝐵 ∧ ∃ℎ ℎ:𝐶–1-1-onto→𝐷)) |
4 | | f1of 6618 |
. . . . . . . 8
⊢ (𝑓:𝐴–1-1-onto→𝐶 → 𝑓:𝐴⟶𝐶) |
5 | | f1odm 6622 |
. . . . . . . . . 10
⊢ (ℎ:𝐶–1-1-onto→𝐷 → dom ℎ = 𝐶) |
6 | | vex 3402 |
. . . . . . . . . . 11
⊢ ℎ ∈ V |
7 | 6 | dmex 7642 |
. . . . . . . . . 10
⊢ dom ℎ ∈ V |
8 | 5, 7 | eqeltrrdi 2842 |
. . . . . . . . 9
⊢ (ℎ:𝐶–1-1-onto→𝐷 → 𝐶 ∈ V) |
9 | | f1odm 6622 |
. . . . . . . . . 10
⊢ (𝑔:𝐴–1-1-onto→𝐵 → dom 𝑔 = 𝐴) |
10 | | vex 3402 |
. . . . . . . . . . 11
⊢ 𝑔 ∈ V |
11 | 10 | dmex 7642 |
. . . . . . . . . 10
⊢ dom 𝑔 ∈ V |
12 | 9, 11 | eqeltrrdi 2842 |
. . . . . . . . 9
⊢ (𝑔:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V) |
13 | | elmapg 8450 |
. . . . . . . . 9
⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝑓 ∈ (𝐶 ↑m 𝐴) ↔ 𝑓:𝐴⟶𝐶)) |
14 | 8, 12, 13 | syl2anr 600 |
. . . . . . . 8
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓 ∈ (𝐶 ↑m 𝐴) ↔ 𝑓:𝐴⟶𝐶)) |
15 | 4, 14 | syl5ibr 249 |
. . . . . . 7
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓:𝐴–1-1-onto→𝐶 → 𝑓 ∈ (𝐶 ↑m 𝐴))) |
16 | 15 | abssdv 3958 |
. . . . . 6
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ⊆ (𝐶 ↑m 𝐴)) |
17 | | ovex 7203 |
. . . . . . 7
⊢ (𝐶 ↑m 𝐴) ∈ V |
18 | 17 | ssex 5189 |
. . . . . 6
⊢ ({𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ⊆ (𝐶 ↑m 𝐴) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∈ V) |
19 | 16, 18 | syl 17 |
. . . . 5
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∈ V) |
20 | | f1of 6618 |
. . . . . . . 8
⊢ (𝑓:𝐵–1-1-onto→𝐷 → 𝑓:𝐵⟶𝐷) |
21 | | f1ofo 6625 |
. . . . . . . . . . 11
⊢ (ℎ:𝐶–1-1-onto→𝐷 → ℎ:𝐶–onto→𝐷) |
22 | | forn 6595 |
. . . . . . . . . . 11
⊢ (ℎ:𝐶–onto→𝐷 → ran ℎ = 𝐷) |
23 | 21, 22 | syl 17 |
. . . . . . . . . 10
⊢ (ℎ:𝐶–1-1-onto→𝐷 → ran ℎ = 𝐷) |
24 | 6 | rnex 7643 |
. . . . . . . . . 10
⊢ ran ℎ ∈ V |
25 | 23, 24 | eqeltrrdi 2842 |
. . . . . . . . 9
⊢ (ℎ:𝐶–1-1-onto→𝐷 → 𝐷 ∈ V) |
26 | | f1ofo 6625 |
. . . . . . . . . . 11
⊢ (𝑔:𝐴–1-1-onto→𝐵 → 𝑔:𝐴–onto→𝐵) |
27 | | forn 6595 |
. . . . . . . . . . 11
⊢ (𝑔:𝐴–onto→𝐵 → ran 𝑔 = 𝐵) |
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
⊢ (𝑔:𝐴–1-1-onto→𝐵 → ran 𝑔 = 𝐵) |
29 | 10 | rnex 7643 |
. . . . . . . . . 10
⊢ ran 𝑔 ∈ V |
30 | 28, 29 | eqeltrrdi 2842 |
. . . . . . . . 9
⊢ (𝑔:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V) |
31 | | elmapg 8450 |
. . . . . . . . 9
⊢ ((𝐷 ∈ V ∧ 𝐵 ∈ V) → (𝑓 ∈ (𝐷 ↑m 𝐵) ↔ 𝑓:𝐵⟶𝐷)) |
32 | 25, 30, 31 | syl2anr 600 |
. . . . . . . 8
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓 ∈ (𝐷 ↑m 𝐵) ↔ 𝑓:𝐵⟶𝐷)) |
33 | 20, 32 | syl5ibr 249 |
. . . . . . 7
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓:𝐵–1-1-onto→𝐷 → 𝑓 ∈ (𝐷 ↑m 𝐵))) |
34 | 33 | abssdv 3958 |
. . . . . 6
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ⊆ (𝐷 ↑m 𝐵)) |
35 | | ovex 7203 |
. . . . . . 7
⊢ (𝐷 ↑m 𝐵) ∈ V |
36 | 35 | ssex 5189 |
. . . . . 6
⊢ ({𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ⊆ (𝐷 ↑m 𝐵) → {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ∈ V) |
37 | 34, 36 | syl 17 |
. . . . 5
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ∈ V) |
38 | | f1oco 6640 |
. . . . . . . . 9
⊢ ((ℎ:𝐶–1-1-onto→𝐷 ∧ 𝑥:𝐴–1-1-onto→𝐶) → (ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷) |
39 | 38 | adantll 714 |
. . . . . . . 8
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐴–1-1-onto→𝐶) → (ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷) |
40 | | f1ocnv 6630 |
. . . . . . . . 9
⊢ (𝑔:𝐴–1-1-onto→𝐵 → ◡𝑔:𝐵–1-1-onto→𝐴) |
41 | 40 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐴–1-1-onto→𝐶) → ◡𝑔:𝐵–1-1-onto→𝐴) |
42 | | f1oco 6640 |
. . . . . . . 8
⊢ (((ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷 ∧ ◡𝑔:𝐵–1-1-onto→𝐴) → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷) |
43 | 39, 41, 42 | syl2anc 587 |
. . . . . . 7
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐴–1-1-onto→𝐶) → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷) |
44 | 43 | ex 416 |
. . . . . 6
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑥:𝐴–1-1-onto→𝐶 → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)) |
45 | | vex 3402 |
. . . . . . 7
⊢ 𝑥 ∈ V |
46 | | f1oeq1 6606 |
. . . . . . 7
⊢ (𝑓 = 𝑥 → (𝑓:𝐴–1-1-onto→𝐶 ↔ 𝑥:𝐴–1-1-onto→𝐶)) |
47 | 45, 46 | elab 3573 |
. . . . . 6
⊢ (𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ↔ 𝑥:𝐴–1-1-onto→𝐶) |
48 | 6, 45 | coex 7661 |
. . . . . . . 8
⊢ (ℎ ∘ 𝑥) ∈ V |
49 | 10 | cnvex 7656 |
. . . . . . . 8
⊢ ◡𝑔 ∈ V |
50 | 48, 49 | coex 7661 |
. . . . . . 7
⊢ ((ℎ ∘ 𝑥) ∘ ◡𝑔) ∈ V |
51 | | f1oeq1 6606 |
. . . . . . 7
⊢ (𝑓 = ((ℎ ∘ 𝑥) ∘ ◡𝑔) → (𝑓:𝐵–1-1-onto→𝐷 ↔ ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)) |
52 | 50, 51 | elab 3573 |
. . . . . 6
⊢ (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ↔ ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷) |
53 | 44, 47, 52 | 3imtr4g 299 |
. . . . 5
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} → ((ℎ ∘ 𝑥) ∘ ◡𝑔) ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})) |
54 | | f1ocnv 6630 |
. . . . . . . . 9
⊢ (ℎ:𝐶–1-1-onto→𝐷 → ◡ℎ:𝐷–1-1-onto→𝐶) |
55 | 54 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐵–1-1-onto→𝐷) → ◡ℎ:𝐷–1-1-onto→𝐶) |
56 | | f1oco 6640 |
. . . . . . . . . 10
⊢ ((𝑦:𝐵–1-1-onto→𝐷 ∧ 𝑔:𝐴–1-1-onto→𝐵) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷) |
57 | 56 | ancoms 462 |
. . . . . . . . 9
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷) |
58 | 57 | adantlr 715 |
. . . . . . . 8
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷) |
59 | | f1oco 6640 |
. . . . . . . 8
⊢ ((◡ℎ:𝐷–1-1-onto→𝐶 ∧ (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶) |
60 | 55, 58, 59 | syl2anc 587 |
. . . . . . 7
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐵–1-1-onto→𝐷) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶) |
61 | 60 | ex 416 |
. . . . . 6
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑦:𝐵–1-1-onto→𝐷 → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)) |
62 | | vex 3402 |
. . . . . . 7
⊢ 𝑦 ∈ V |
63 | | f1oeq1 6606 |
. . . . . . 7
⊢ (𝑓 = 𝑦 → (𝑓:𝐵–1-1-onto→𝐷 ↔ 𝑦:𝐵–1-1-onto→𝐷)) |
64 | 62, 63 | elab 3573 |
. . . . . 6
⊢ (𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ↔ 𝑦:𝐵–1-1-onto→𝐷) |
65 | 6 | cnvex 7656 |
. . . . . . . 8
⊢ ◡ℎ ∈ V |
66 | 62, 10 | coex 7661 |
. . . . . . . 8
⊢ (𝑦 ∘ 𝑔) ∈ V |
67 | 65, 66 | coex 7661 |
. . . . . . 7
⊢ (◡ℎ ∘ (𝑦 ∘ 𝑔)) ∈ V |
68 | | f1oeq1 6606 |
. . . . . . 7
⊢ (𝑓 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) → (𝑓:𝐴–1-1-onto→𝐶 ↔ (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)) |
69 | 67, 68 | elab 3573 |
. . . . . 6
⊢ ((◡ℎ ∘ (𝑦 ∘ 𝑔)) ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ↔ (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶) |
70 | 61, 64, 69 | 3imtr4g 299 |
. . . . 5
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} → (◡ℎ ∘ (𝑦 ∘ 𝑔)) ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶})) |
71 | 47, 64 | anbi12i 630 |
. . . . . 6
⊢ ((𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∧ 𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) ↔ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) |
72 | | coass 6098 |
. . . . . . . . . . 11
⊢ (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = ((ℎ ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) |
73 | | f1ococnv1 6646 |
. . . . . . . . . . . . . 14
⊢ (𝑔:𝐴–1-1-onto→𝐵 → (◡𝑔 ∘ 𝑔) = ( I ↾ 𝐴)) |
74 | 73 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (◡𝑔 ∘ 𝑔) = ( I ↾ 𝐴)) |
75 | 74 | coeq2d 5705 |
. . . . . . . . . . . 12
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) = ((ℎ ∘ 𝑥) ∘ ( I ↾ 𝐴))) |
76 | 39 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷) |
77 | | f1of 6618 |
. . . . . . . . . . . . 13
⊢ ((ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷 → (ℎ ∘ 𝑥):𝐴⟶𝐷) |
78 | | fcoi1 6552 |
. . . . . . . . . . . . 13
⊢ ((ℎ ∘ 𝑥):𝐴⟶𝐷 → ((ℎ ∘ 𝑥) ∘ ( I ↾ 𝐴)) = (ℎ ∘ 𝑥)) |
79 | 76, 77, 78 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ ( I ↾ 𝐴)) = (ℎ ∘ 𝑥)) |
80 | 75, 79 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) = (ℎ ∘ 𝑥)) |
81 | 72, 80 | eqtr2id 2786 |
. . . . . . . . . 10
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ 𝑥) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔)) |
82 | | coass 6098 |
. . . . . . . . . . 11
⊢ ((ℎ ∘ ◡ℎ) ∘ (𝑦 ∘ 𝑔)) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) |
83 | | f1ococnv2 6644 |
. . . . . . . . . . . . . 14
⊢ (ℎ:𝐶–1-1-onto→𝐷 → (ℎ ∘ ◡ℎ) = ( I ↾ 𝐷)) |
84 | 83 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ ◡ℎ) = ( I ↾ 𝐷)) |
85 | 84 | coeq1d 5704 |
. . . . . . . . . . . 12
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ ◡ℎ) ∘ (𝑦 ∘ 𝑔)) = (( I ↾ 𝐷) ∘ (𝑦 ∘ 𝑔))) |
86 | 58 | adantrl 716 |
. . . . . . . . . . . . 13
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷) |
87 | | f1of 6618 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷 → (𝑦 ∘ 𝑔):𝐴⟶𝐷) |
88 | | fcoi2 6553 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∘ 𝑔):𝐴⟶𝐷 → (( I ↾ 𝐷) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔)) |
89 | 86, 87, 88 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (( I ↾ 𝐷) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔)) |
90 | 85, 89 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ ◡ℎ) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔)) |
91 | 82, 90 | eqtr3id 2787 |
. . . . . . . . . 10
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) = (𝑦 ∘ 𝑔)) |
92 | 81, 91 | eqeq12d 2754 |
. . . . . . . . 9
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = (𝑦 ∘ 𝑔))) |
93 | | eqcom 2745 |
. . . . . . . . 9
⊢ ((((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = (𝑦 ∘ 𝑔) ↔ (𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔)) |
94 | 92, 93 | bitrdi 290 |
. . . . . . . 8
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ (𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔))) |
95 | | f1of1 6617 |
. . . . . . . . . 10
⊢ (ℎ:𝐶–1-1-onto→𝐷 → ℎ:𝐶–1-1→𝐷) |
96 | 95 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ℎ:𝐶–1-1→𝐷) |
97 | | f1of 6618 |
. . . . . . . . . 10
⊢ (𝑥:𝐴–1-1-onto→𝐶 → 𝑥:𝐴⟶𝐶) |
98 | 97 | ad2antrl 728 |
. . . . . . . . 9
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → 𝑥:𝐴⟶𝐶) |
99 | 60 | adantrl 716 |
. . . . . . . . . 10
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶) |
100 | | f1of 6618 |
. . . . . . . . . 10
⊢ ((◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶 → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴⟶𝐶) |
101 | 99, 100 | syl 17 |
. . . . . . . . 9
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴⟶𝐶) |
102 | | cocan1 7058 |
. . . . . . . . 9
⊢ ((ℎ:𝐶–1-1→𝐷 ∧ 𝑥:𝐴⟶𝐶 ∧ (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴⟶𝐶) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ 𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)))) |
103 | 96, 98, 101, 102 | syl3anc 1372 |
. . . . . . . 8
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ 𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)))) |
104 | 26 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → 𝑔:𝐴–onto→𝐵) |
105 | | f1ofn 6619 |
. . . . . . . . . 10
⊢ (𝑦:𝐵–1-1-onto→𝐷 → 𝑦 Fn 𝐵) |
106 | 105 | ad2antll 729 |
. . . . . . . . 9
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → 𝑦 Fn 𝐵) |
107 | 43 | adantrr 717 |
. . . . . . . . . 10
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷) |
108 | | f1ofn 6619 |
. . . . . . . . . 10
⊢ (((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷 → ((ℎ ∘ 𝑥) ∘ ◡𝑔) Fn 𝐵) |
109 | 107, 108 | syl 17 |
. . . . . . . . 9
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ ◡𝑔) Fn 𝐵) |
110 | | cocan2 7059 |
. . . . . . . . 9
⊢ ((𝑔:𝐴–onto→𝐵 ∧ 𝑦 Fn 𝐵 ∧ ((ℎ ∘ 𝑥) ∘ ◡𝑔) Fn 𝐵) → ((𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔))) |
111 | 104, 106,
109, 110 | syl3anc 1372 |
. . . . . . . 8
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔))) |
112 | 94, 103, 111 | 3bitr3d 312 |
. . . . . . 7
⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔))) |
113 | 112 | ex 416 |
. . . . . 6
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → ((𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔)))) |
114 | 71, 113 | syl5bi 245 |
. . . . 5
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → ((𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∧ 𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) → (𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔)))) |
115 | 19, 37, 53, 70, 114 | en3d 8592 |
. . . 4
⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) |
116 | 115 | exlimivv 1939 |
. . 3
⊢
(∃𝑔∃ℎ(𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) |
117 | 3, 116 | sylbir 238 |
. 2
⊢
((∃𝑔 𝑔:𝐴–1-1-onto→𝐵 ∧ ∃ℎ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) |
118 | 1, 2, 117 | syl2anb 601 |
1
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) |