Step | Hyp | Ref
| Expression |
1 | | bren 8564 |
. . 3
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
2 | | f1odm 6622 |
. . . . . . 7
⊢ (𝑓:𝐴–1-1-onto→𝐵 → dom 𝑓 = 𝐴) |
3 | | vex 3402 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
4 | 3 | dmex 7642 |
. . . . . . 7
⊢ dom 𝑓 ∈ V |
5 | 2, 4 | eqeltrrdi 2842 |
. . . . . 6
⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V) |
6 | | pwexg 5245 |
. . . . . 6
⊢ (𝐴 ∈ V → 𝒫 𝐴 ∈ V) |
7 | | inex1g 5187 |
. . . . . 6
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴 ∩
{𝑥 ∣ 𝑥 ≈ 𝐶}) ∈ V) |
8 | 5, 6, 7 | 3syl 18 |
. . . . 5
⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ∈ V) |
9 | | f1ofo 6625 |
. . . . . . . 8
⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵) |
10 | | forn 6595 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵) |
12 | 3 | rnex 7643 |
. . . . . . 7
⊢ ran 𝑓 ∈ V |
13 | 11, 12 | eqeltrrdi 2842 |
. . . . . 6
⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V) |
14 | | pwexg 5245 |
. . . . . 6
⊢ (𝐵 ∈ V → 𝒫 𝐵 ∈ V) |
15 | | inex1g 5187 |
. . . . . 6
⊢
(𝒫 𝐵 ∈
V → (𝒫 𝐵 ∩
{𝑥 ∣ 𝑥 ≈ 𝐶}) ∈ V) |
16 | 13, 14, 15 | 3syl 18 |
. . . . 5
⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ∈ V) |
17 | | f1of1 6617 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–1-1→𝐵) |
18 | 17 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑦 ⊆ 𝐴) → 𝑓:𝐴–1-1→𝐵) |
19 | 13 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑦 ⊆ 𝐴) → 𝐵 ∈ V) |
20 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ 𝐴) |
21 | | vex 3402 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
22 | 21 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑦 ⊆ 𝐴) → 𝑦 ∈ V) |
23 | | f1imaen2g 8616 |
. . . . . . . . . 10
⊢ (((𝑓:𝐴–1-1→𝐵 ∧ 𝐵 ∈ V) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ V)) → (𝑓 “ 𝑦) ≈ 𝑦) |
24 | 18, 19, 20, 22, 23 | syl22anc 838 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑦 ⊆ 𝐴) → (𝑓 “ 𝑦) ≈ 𝑦) |
25 | | entr 8607 |
. . . . . . . . 9
⊢ (((𝑓 “ 𝑦) ≈ 𝑦 ∧ 𝑦 ≈ 𝐶) → (𝑓 “ 𝑦) ≈ 𝐶) |
26 | 24, 25 | sylan 583 |
. . . . . . . 8
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑦 ⊆ 𝐴) ∧ 𝑦 ≈ 𝐶) → (𝑓 “ 𝑦) ≈ 𝐶) |
27 | 26 | expl 461 |
. . . . . . 7
⊢ (𝑓:𝐴–1-1-onto→𝐵 → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝐶) → (𝑓 “ 𝑦) ≈ 𝐶)) |
28 | | imassrn 5914 |
. . . . . . . . 9
⊢ (𝑓 “ 𝑦) ⊆ ran 𝑓 |
29 | 28, 10 | sseqtrid 3929 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→𝐵 → (𝑓 “ 𝑦) ⊆ 𝐵) |
30 | 9, 29 | syl 17 |
. . . . . . 7
⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝑓 “ 𝑦) ⊆ 𝐵) |
31 | 27, 30 | jctild 529 |
. . . . . 6
⊢ (𝑓:𝐴–1-1-onto→𝐵 → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝐶) → ((𝑓 “ 𝑦) ⊆ 𝐵 ∧ (𝑓 “ 𝑦) ≈ 𝐶))) |
32 | | elin 3859 |
. . . . . . 7
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ↔ (𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝑥 ≈ 𝐶})) |
33 | 21 | elpw 4492 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴) |
34 | | breq1 5033 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝐶 ↔ 𝑦 ≈ 𝐶)) |
35 | 21, 34 | elab 3573 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑥 ∣ 𝑥 ≈ 𝐶} ↔ 𝑦 ≈ 𝐶) |
36 | 33, 35 | anbi12i 630 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝑥 ≈ 𝐶}) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝐶)) |
37 | 32, 36 | bitri 278 |
. . . . . 6
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝐶)) |
38 | | elin 3859 |
. . . . . . 7
⊢ ((𝑓 “ 𝑦) ∈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ↔ ((𝑓 “ 𝑦) ∈ 𝒫 𝐵 ∧ (𝑓 “ 𝑦) ∈ {𝑥 ∣ 𝑥 ≈ 𝐶})) |
39 | 3 | imaex 7647 |
. . . . . . . . 9
⊢ (𝑓 “ 𝑦) ∈ V |
40 | 39 | elpw 4492 |
. . . . . . . 8
⊢ ((𝑓 “ 𝑦) ∈ 𝒫 𝐵 ↔ (𝑓 “ 𝑦) ⊆ 𝐵) |
41 | | breq1 5033 |
. . . . . . . . 9
⊢ (𝑥 = (𝑓 “ 𝑦) → (𝑥 ≈ 𝐶 ↔ (𝑓 “ 𝑦) ≈ 𝐶)) |
42 | 39, 41 | elab 3573 |
. . . . . . . 8
⊢ ((𝑓 “ 𝑦) ∈ {𝑥 ∣ 𝑥 ≈ 𝐶} ↔ (𝑓 “ 𝑦) ≈ 𝐶) |
43 | 40, 42 | anbi12i 630 |
. . . . . . 7
⊢ (((𝑓 “ 𝑦) ∈ 𝒫 𝐵 ∧ (𝑓 “ 𝑦) ∈ {𝑥 ∣ 𝑥 ≈ 𝐶}) ↔ ((𝑓 “ 𝑦) ⊆ 𝐵 ∧ (𝑓 “ 𝑦) ≈ 𝐶)) |
44 | 38, 43 | bitri 278 |
. . . . . 6
⊢ ((𝑓 “ 𝑦) ∈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ↔ ((𝑓 “ 𝑦) ⊆ 𝐵 ∧ (𝑓 “ 𝑦) ≈ 𝐶)) |
45 | 31, 37, 44 | 3imtr4g 299 |
. . . . 5
⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝑦 ∈ (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) → (𝑓 “ 𝑦) ∈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}))) |
46 | | f1ocnv 6630 |
. . . . . . 7
⊢ (𝑓:𝐴–1-1-onto→𝐵 → ◡𝑓:𝐵–1-1-onto→𝐴) |
47 | | f1of1 6617 |
. . . . . . . . . . . 12
⊢ (◡𝑓:𝐵–1-1-onto→𝐴 → ◡𝑓:𝐵–1-1→𝐴) |
48 | | f1f1orn 6629 |
. . . . . . . . . . . 12
⊢ (◡𝑓:𝐵–1-1→𝐴 → ◡𝑓:𝐵–1-1-onto→ran
◡𝑓) |
49 | | f1of1 6617 |
. . . . . . . . . . . 12
⊢ (◡𝑓:𝐵–1-1-onto→ran
◡𝑓 → ◡𝑓:𝐵–1-1→ran ◡𝑓) |
50 | 47, 48, 49 | 3syl 18 |
. . . . . . . . . . 11
⊢ (◡𝑓:𝐵–1-1-onto→𝐴 → ◡𝑓:𝐵–1-1→ran ◡𝑓) |
51 | | vex 3402 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
52 | 51 | f1imaen 8617 |
. . . . . . . . . . 11
⊢ ((◡𝑓:𝐵–1-1→ran ◡𝑓 ∧ 𝑧 ⊆ 𝐵) → (◡𝑓 “ 𝑧) ≈ 𝑧) |
53 | 50, 52 | sylan 583 |
. . . . . . . . . 10
⊢ ((◡𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑧 ⊆ 𝐵) → (◡𝑓 “ 𝑧) ≈ 𝑧) |
54 | | entr 8607 |
. . . . . . . . . 10
⊢ (((◡𝑓 “ 𝑧) ≈ 𝑧 ∧ 𝑧 ≈ 𝐶) → (◡𝑓 “ 𝑧) ≈ 𝐶) |
55 | 53, 54 | sylan 583 |
. . . . . . . . 9
⊢ (((◡𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑧 ⊆ 𝐵) ∧ 𝑧 ≈ 𝐶) → (◡𝑓 “ 𝑧) ≈ 𝐶) |
56 | 55 | expl 461 |
. . . . . . . 8
⊢ (◡𝑓:𝐵–1-1-onto→𝐴 → ((𝑧 ⊆ 𝐵 ∧ 𝑧 ≈ 𝐶) → (◡𝑓 “ 𝑧) ≈ 𝐶)) |
57 | | f1ofo 6625 |
. . . . . . . . 9
⊢ (◡𝑓:𝐵–1-1-onto→𝐴 → ◡𝑓:𝐵–onto→𝐴) |
58 | | imassrn 5914 |
. . . . . . . . . 10
⊢ (◡𝑓 “ 𝑧) ⊆ ran ◡𝑓 |
59 | | forn 6595 |
. . . . . . . . . 10
⊢ (◡𝑓:𝐵–onto→𝐴 → ran ◡𝑓 = 𝐴) |
60 | 58, 59 | sseqtrid 3929 |
. . . . . . . . 9
⊢ (◡𝑓:𝐵–onto→𝐴 → (◡𝑓 “ 𝑧) ⊆ 𝐴) |
61 | 57, 60 | syl 17 |
. . . . . . . 8
⊢ (◡𝑓:𝐵–1-1-onto→𝐴 → (◡𝑓 “ 𝑧) ⊆ 𝐴) |
62 | 56, 61 | jctild 529 |
. . . . . . 7
⊢ (◡𝑓:𝐵–1-1-onto→𝐴 → ((𝑧 ⊆ 𝐵 ∧ 𝑧 ≈ 𝐶) → ((◡𝑓 “ 𝑧) ⊆ 𝐴 ∧ (◡𝑓 “ 𝑧) ≈ 𝐶))) |
63 | 46, 62 | syl 17 |
. . . . . 6
⊢ (𝑓:𝐴–1-1-onto→𝐵 → ((𝑧 ⊆ 𝐵 ∧ 𝑧 ≈ 𝐶) → ((◡𝑓 “ 𝑧) ⊆ 𝐴 ∧ (◡𝑓 “ 𝑧) ≈ 𝐶))) |
64 | | elin 3859 |
. . . . . . 7
⊢ (𝑧 ∈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ↔ (𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ∈ {𝑥 ∣ 𝑥 ≈ 𝐶})) |
65 | 51 | elpw 4492 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝒫 𝐵 ↔ 𝑧 ⊆ 𝐵) |
66 | | breq1 5033 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 ≈ 𝐶 ↔ 𝑧 ≈ 𝐶)) |
67 | 51, 66 | elab 3573 |
. . . . . . . 8
⊢ (𝑧 ∈ {𝑥 ∣ 𝑥 ≈ 𝐶} ↔ 𝑧 ≈ 𝐶) |
68 | 65, 67 | anbi12i 630 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ∈ {𝑥 ∣ 𝑥 ≈ 𝐶}) ↔ (𝑧 ⊆ 𝐵 ∧ 𝑧 ≈ 𝐶)) |
69 | 64, 68 | bitri 278 |
. . . . . 6
⊢ (𝑧 ∈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ↔ (𝑧 ⊆ 𝐵 ∧ 𝑧 ≈ 𝐶)) |
70 | | elin 3859 |
. . . . . . 7
⊢ ((◡𝑓 “ 𝑧) ∈ (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ↔ ((◡𝑓 “ 𝑧) ∈ 𝒫 𝐴 ∧ (◡𝑓 “ 𝑧) ∈ {𝑥 ∣ 𝑥 ≈ 𝐶})) |
71 | 3 | cnvex 7656 |
. . . . . . . . . 10
⊢ ◡𝑓 ∈ V |
72 | 71 | imaex 7647 |
. . . . . . . . 9
⊢ (◡𝑓 “ 𝑧) ∈ V |
73 | 72 | elpw 4492 |
. . . . . . . 8
⊢ ((◡𝑓 “ 𝑧) ∈ 𝒫 𝐴 ↔ (◡𝑓 “ 𝑧) ⊆ 𝐴) |
74 | | breq1 5033 |
. . . . . . . . 9
⊢ (𝑥 = (◡𝑓 “ 𝑧) → (𝑥 ≈ 𝐶 ↔ (◡𝑓 “ 𝑧) ≈ 𝐶)) |
75 | 72, 74 | elab 3573 |
. . . . . . . 8
⊢ ((◡𝑓 “ 𝑧) ∈ {𝑥 ∣ 𝑥 ≈ 𝐶} ↔ (◡𝑓 “ 𝑧) ≈ 𝐶) |
76 | 73, 75 | anbi12i 630 |
. . . . . . 7
⊢ (((◡𝑓 “ 𝑧) ∈ 𝒫 𝐴 ∧ (◡𝑓 “ 𝑧) ∈ {𝑥 ∣ 𝑥 ≈ 𝐶}) ↔ ((◡𝑓 “ 𝑧) ⊆ 𝐴 ∧ (◡𝑓 “ 𝑧) ≈ 𝐶)) |
77 | 70, 76 | bitri 278 |
. . . . . 6
⊢ ((◡𝑓 “ 𝑧) ∈ (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ↔ ((◡𝑓 “ 𝑧) ⊆ 𝐴 ∧ (◡𝑓 “ 𝑧) ≈ 𝐶)) |
78 | 63, 69, 77 | 3imtr4g 299 |
. . . . 5
⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝑧 ∈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) → (◡𝑓 “ 𝑧) ∈ (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}))) |
79 | | simpl 486 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ∈ {𝑥 ∣ 𝑥 ≈ 𝐶}) → 𝑧 ∈ 𝒫 𝐵) |
80 | 79 | elpwid 4499 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ∈ {𝑥 ∣ 𝑥 ≈ 𝐶}) → 𝑧 ⊆ 𝐵) |
81 | 64, 80 | sylbi 220 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) → 𝑧 ⊆ 𝐵) |
82 | | imaeq2 5899 |
. . . . . . . . . . . 12
⊢ (𝑦 = (◡𝑓 “ 𝑧) → (𝑓 “ 𝑦) = (𝑓 “ (◡𝑓 “ 𝑧))) |
83 | | f1orel 6621 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝐴–1-1-onto→𝐵 → Rel 𝑓) |
84 | | dfrel2 6021 |
. . . . . . . . . . . . . . . 16
⊢ (Rel
𝑓 ↔ ◡◡𝑓 = 𝑓) |
85 | 83, 84 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐴–1-1-onto→𝐵 → ◡◡𝑓 = 𝑓) |
86 | 85 | imaeq1d 5902 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–1-1-onto→𝐵 → (◡◡𝑓 “ (◡𝑓 “ 𝑧)) = (𝑓 “ (◡𝑓 “ 𝑧))) |
87 | 86 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑧 ⊆ 𝐵) → (◡◡𝑓 “ (◡𝑓 “ 𝑧)) = (𝑓 “ (◡𝑓 “ 𝑧))) |
88 | 46, 47 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–1-1-onto→𝐵 → ◡𝑓:𝐵–1-1→𝐴) |
89 | | f1imacnv 6634 |
. . . . . . . . . . . . . 14
⊢ ((◡𝑓:𝐵–1-1→𝐴 ∧ 𝑧 ⊆ 𝐵) → (◡◡𝑓 “ (◡𝑓 “ 𝑧)) = 𝑧) |
90 | 88, 89 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑧 ⊆ 𝐵) → (◡◡𝑓 “ (◡𝑓 “ 𝑧)) = 𝑧) |
91 | 87, 90 | eqtr3d 2775 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑧 ⊆ 𝐵) → (𝑓 “ (◡𝑓 “ 𝑧)) = 𝑧) |
92 | 82, 91 | sylan9eqr 2795 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑧 ⊆ 𝐵) ∧ 𝑦 = (◡𝑓 “ 𝑧)) → (𝑓 “ 𝑦) = 𝑧) |
93 | 92 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑧 ⊆ 𝐵) ∧ 𝑦 = (◡𝑓 “ 𝑧)) → 𝑧 = (𝑓 “ 𝑦)) |
94 | 93 | ex 416 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑧 ⊆ 𝐵) → (𝑦 = (◡𝑓 “ 𝑧) → 𝑧 = (𝑓 “ 𝑦))) |
95 | 81, 94 | sylan2 596 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑧 ∈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶})) → (𝑦 = (◡𝑓 “ 𝑧) → 𝑧 = (𝑓 “ 𝑦))) |
96 | 95 | adantrl 716 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ∧ 𝑧 ∈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}))) → (𝑦 = (◡𝑓 “ 𝑧) → 𝑧 = (𝑓 “ 𝑦))) |
97 | | simpl 486 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝑥 ≈ 𝐶}) → 𝑦 ∈ 𝒫 𝐴) |
98 | 97 | elpwid 4499 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝑥 ≈ 𝐶}) → 𝑦 ⊆ 𝐴) |
99 | 32, 98 | sylbi 220 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) → 𝑦 ⊆ 𝐴) |
100 | | imaeq2 5899 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑓 “ 𝑦) → (◡𝑓 “ 𝑧) = (◡𝑓 “ (𝑓 “ 𝑦))) |
101 | | f1imacnv 6634 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑦 ⊆ 𝐴) → (◡𝑓 “ (𝑓 “ 𝑦)) = 𝑦) |
102 | 17, 101 | sylan 583 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑦 ⊆ 𝐴) → (◡𝑓 “ (𝑓 “ 𝑦)) = 𝑦) |
103 | 100, 102 | sylan9eqr 2795 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑦 ⊆ 𝐴) ∧ 𝑧 = (𝑓 “ 𝑦)) → (◡𝑓 “ 𝑧) = 𝑦) |
104 | 103 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑦 ⊆ 𝐴) ∧ 𝑧 = (𝑓 “ 𝑦)) → 𝑦 = (◡𝑓 “ 𝑧)) |
105 | 104 | ex 416 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑦 ⊆ 𝐴) → (𝑧 = (𝑓 “ 𝑦) → 𝑦 = (◡𝑓 “ 𝑧))) |
106 | 99, 105 | sylan2 596 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶})) → (𝑧 = (𝑓 “ 𝑦) → 𝑦 = (◡𝑓 “ 𝑧))) |
107 | 106 | adantrr 717 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ∧ 𝑧 ∈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}))) → (𝑧 = (𝑓 “ 𝑦) → 𝑦 = (◡𝑓 “ 𝑧))) |
108 | 96, 107 | impbid 215 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→𝐵 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ∧ 𝑧 ∈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}))) → (𝑦 = (◡𝑓 “ 𝑧) ↔ 𝑧 = (𝑓 “ 𝑦))) |
109 | 108 | ex 416 |
. . . . 5
⊢ (𝑓:𝐴–1-1-onto→𝐵 → ((𝑦 ∈ (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ∧ 𝑧 ∈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶})) → (𝑦 = (◡𝑓 “ 𝑧) ↔ 𝑧 = (𝑓 “ 𝑦)))) |
110 | 8, 16, 45, 78, 109 | en3d 8592 |
. . . 4
⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ≈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶})) |
111 | 110 | exlimiv 1937 |
. . 3
⊢
(∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ≈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶})) |
112 | 1, 111 | sylbi 220 |
. 2
⊢ (𝐴 ≈ 𝐵 → (𝒫 𝐴 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) ≈ (𝒫 𝐵 ∩ {𝑥 ∣ 𝑥 ≈ 𝐶})) |
113 | | df-pw 4490 |
. . . 4
⊢ 𝒫
𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} |
114 | 113 | ineq1i 4099 |
. . 3
⊢
(𝒫 𝐴 ∩
{𝑥 ∣ 𝑥 ≈ 𝐶}) = ({𝑥 ∣ 𝑥 ⊆ 𝐴} ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) |
115 | | inab 4189 |
. . 3
⊢ ({𝑥 ∣ 𝑥 ⊆ 𝐴} ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶)} |
116 | 114, 115 | eqtri 2761 |
. 2
⊢
(𝒫 𝐴 ∩
{𝑥 ∣ 𝑥 ≈ 𝐶}) = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶)} |
117 | | df-pw 4490 |
. . . 4
⊢ 𝒫
𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵} |
118 | 117 | ineq1i 4099 |
. . 3
⊢
(𝒫 𝐵 ∩
{𝑥 ∣ 𝑥 ≈ 𝐶}) = ({𝑥 ∣ 𝑥 ⊆ 𝐵} ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) |
119 | | inab 4189 |
. . 3
⊢ ({𝑥 ∣ 𝑥 ⊆ 𝐵} ∩ {𝑥 ∣ 𝑥 ≈ 𝐶}) = {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶)} |
120 | 118, 119 | eqtri 2761 |
. 2
⊢
(𝒫 𝐵 ∩
{𝑥 ∣ 𝑥 ≈ 𝐶}) = {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶)} |
121 | 112, 116,
120 | 3brtr3g 5063 |
1
⊢ (𝐴 ≈ 𝐵 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶)} ≈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶)}) |