Proof of Theorem f1opw2
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. 2
⊢ (𝑏 ∈ 𝒫 𝐴 ↦ (𝐹 “ 𝑏)) = (𝑏 ∈ 𝒫 𝐴 ↦ (𝐹 “ 𝑏)) |
2 | | imassrn 5477 |
. . . . 5
⊢ (𝐹 “ 𝑏) ⊆ ran 𝐹 |
3 | | f1opw2.1 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) |
4 | | f1ofo 6144 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐴–onto→𝐵) |
6 | | forn 6118 |
. . . . . 6
⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝐹 = 𝐵) |
8 | 2, 7 | syl5sseq 3653 |
. . . 4
⊢ (𝜑 → (𝐹 “ 𝑏) ⊆ 𝐵) |
9 | | f1opw2.3 |
. . . . 5
⊢ (𝜑 → (𝐹 “ 𝑏) ∈ V) |
10 | | elpwg 4166 |
. . . . 5
⊢ ((𝐹 “ 𝑏) ∈ V → ((𝐹 “ 𝑏) ∈ 𝒫 𝐵 ↔ (𝐹 “ 𝑏) ⊆ 𝐵)) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐹 “ 𝑏) ∈ 𝒫 𝐵 ↔ (𝐹 “ 𝑏) ⊆ 𝐵)) |
12 | 8, 11 | mpbird 247 |
. . 3
⊢ (𝜑 → (𝐹 “ 𝑏) ∈ 𝒫 𝐵) |
13 | 12 | adantr 481 |
. 2
⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝐹 “ 𝑏) ∈ 𝒫 𝐵) |
14 | | imassrn 5477 |
. . . . 5
⊢ (◡𝐹 “ 𝑎) ⊆ ran ◡𝐹 |
15 | | dfdm4 5316 |
. . . . . 6
⊢ dom 𝐹 = ran ◡𝐹 |
16 | | f1odm 6141 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴) |
17 | 3, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = 𝐴) |
18 | 15, 17 | syl5eqr 2670 |
. . . . 5
⊢ (𝜑 → ran ◡𝐹 = 𝐴) |
19 | 14, 18 | syl5sseq 3653 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ 𝑎) ⊆ 𝐴) |
20 | | f1opw2.2 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ 𝑎) ∈ V) |
21 | | elpwg 4166 |
. . . . 5
⊢ ((◡𝐹 “ 𝑎) ∈ V → ((◡𝐹 “ 𝑎) ∈ 𝒫 𝐴 ↔ (◡𝐹 “ 𝑎) ⊆ 𝐴)) |
22 | 20, 21 | syl 17 |
. . . 4
⊢ (𝜑 → ((◡𝐹 “ 𝑎) ∈ 𝒫 𝐴 ↔ (◡𝐹 “ 𝑎) ⊆ 𝐴)) |
23 | 19, 22 | mpbird 247 |
. . 3
⊢ (𝜑 → (◡𝐹 “ 𝑎) ∈ 𝒫 𝐴) |
24 | 23 | adantr 481 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → (◡𝐹 “ 𝑎) ∈ 𝒫 𝐴) |
25 | | elpwi 4168 |
. . . . . . 7
⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵) |
26 | 25 | adantl 482 |
. . . . . 6
⊢ ((𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵) → 𝑎 ⊆ 𝐵) |
27 | | foimacnv 6154 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑎 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝑎)) = 𝑎) |
28 | 5, 26, 27 | syl2an 494 |
. . . . 5
⊢ ((𝜑 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (𝐹 “ (◡𝐹 “ 𝑎)) = 𝑎) |
29 | 28 | eqcomd 2628 |
. . . 4
⊢ ((𝜑 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → 𝑎 = (𝐹 “ (◡𝐹 “ 𝑎))) |
30 | | imaeq2 5462 |
. . . . 5
⊢ (𝑏 = (◡𝐹 “ 𝑎) → (𝐹 “ 𝑏) = (𝐹 “ (◡𝐹 “ 𝑎))) |
31 | 30 | eqeq2d 2632 |
. . . 4
⊢ (𝑏 = (◡𝐹 “ 𝑎) → (𝑎 = (𝐹 “ 𝑏) ↔ 𝑎 = (𝐹 “ (◡𝐹 “ 𝑎)))) |
32 | 29, 31 | syl5ibrcom 237 |
. . 3
⊢ ((𝜑 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (𝑏 = (◡𝐹 “ 𝑎) → 𝑎 = (𝐹 “ 𝑏))) |
33 | | f1of1 6136 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵) |
34 | 3, 33 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵) |
35 | | elpwi 4168 |
. . . . . . 7
⊢ (𝑏 ∈ 𝒫 𝐴 → 𝑏 ⊆ 𝐴) |
36 | 35 | adantr 481 |
. . . . . 6
⊢ ((𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵) → 𝑏 ⊆ 𝐴) |
37 | | f1imacnv 6153 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑏 ⊆ 𝐴) → (◡𝐹 “ (𝐹 “ 𝑏)) = 𝑏) |
38 | 34, 36, 37 | syl2an 494 |
. . . . 5
⊢ ((𝜑 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (◡𝐹 “ (𝐹 “ 𝑏)) = 𝑏) |
39 | 38 | eqcomd 2628 |
. . . 4
⊢ ((𝜑 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → 𝑏 = (◡𝐹 “ (𝐹 “ 𝑏))) |
40 | | imaeq2 5462 |
. . . . 5
⊢ (𝑎 = (𝐹 “ 𝑏) → (◡𝐹 “ 𝑎) = (◡𝐹 “ (𝐹 “ 𝑏))) |
41 | 40 | eqeq2d 2632 |
. . . 4
⊢ (𝑎 = (𝐹 “ 𝑏) → (𝑏 = (◡𝐹 “ 𝑎) ↔ 𝑏 = (◡𝐹 “ (𝐹 “ 𝑏)))) |
42 | 39, 41 | syl5ibrcom 237 |
. . 3
⊢ ((𝜑 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (𝑎 = (𝐹 “ 𝑏) → 𝑏 = (◡𝐹 “ 𝑎))) |
43 | 32, 42 | impbid 202 |
. 2
⊢ ((𝜑 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (𝑏 = (◡𝐹 “ 𝑎) ↔ 𝑎 = (𝐹 “ 𝑏))) |
44 | 1, 13, 24, 43 | f1o2d 6887 |
1
⊢ (𝜑 → (𝑏 ∈ 𝒫 𝐴 ↦ (𝐹 “ 𝑏)):𝒫 𝐴–1-1-onto→𝒫 𝐵) |