| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. 2
⊢ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹 “ 𝑏)) = (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹 “ 𝑏)) |
| 2 | | simpr 484 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) |
| 3 | 2 | elin2d 4205 |
. . . . 5
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑏 ∈ Fin) |
| 4 | | f1ofun 6850 |
. . . . . 6
⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹) |
| 5 | | elinel1 4201 |
. . . . . . . . 9
⊢ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) → 𝑏 ∈ 𝒫 𝐴) |
| 6 | | elpwi 4607 |
. . . . . . . . 9
⊢ (𝑏 ∈ 𝒫 𝐴 → 𝑏 ⊆ 𝐴) |
| 7 | 5, 6 | syl 17 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) → 𝑏 ⊆ 𝐴) |
| 8 | 7 | adantl 481 |
. . . . . . 7
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑏 ⊆ 𝐴) |
| 9 | | f1odm 6852 |
. . . . . . . 8
⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴) |
| 10 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → dom 𝐹 = 𝐴) |
| 11 | 8, 10 | sseqtrrd 4021 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑏 ⊆ dom 𝐹) |
| 12 | | fores 6830 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝑏 ⊆ dom 𝐹) → (𝐹 ↾ 𝑏):𝑏–onto→(𝐹 “ 𝑏)) |
| 13 | 4, 11, 12 | syl2an2r 685 |
. . . . 5
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑏):𝑏–onto→(𝐹 “ 𝑏)) |
| 14 | | fofi 9351 |
. . . . 5
⊢ ((𝑏 ∈ Fin ∧ (𝐹 ↾ 𝑏):𝑏–onto→(𝐹 “ 𝑏)) → (𝐹 “ 𝑏) ∈ Fin) |
| 15 | 3, 13, 14 | syl2anc 584 |
. . . 4
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ 𝑏) ∈ Fin) |
| 16 | | imassrn 6089 |
. . . . . 6
⊢ (𝐹 “ 𝑏) ⊆ ran 𝐹 |
| 17 | | f1ofo 6855 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵) |
| 18 | | forn 6823 |
. . . . . . 7
⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) |
| 19 | 17, 18 | syl 17 |
. . . . . 6
⊢ (𝐹:𝐴–1-1-onto→𝐵 → ran 𝐹 = 𝐵) |
| 20 | 16, 19 | sseqtrid 4026 |
. . . . 5
⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 “ 𝑏) ⊆ 𝐵) |
| 21 | 20 | adantr 480 |
. . . 4
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ 𝑏) ⊆ 𝐵) |
| 22 | 15, 21 | elpwd 4606 |
. . 3
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ 𝑏) ∈ 𝒫 𝐵) |
| 23 | 22, 15 | elind 4200 |
. 2
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ 𝑏) ∈ (𝒫 𝐵 ∩ Fin)) |
| 24 | | simpr 484 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) |
| 25 | 24 | elin2d 4205 |
. . . . 5
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ Fin) |
| 26 | | dff1o3 6854 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹)) |
| 27 | 26 | simprbi 496 |
. . . . . 6
⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun ◡𝐹) |
| 28 | | elinel1 4201 |
. . . . . . . . 9
⊢ (𝑎 ∈ (𝒫 𝐵 ∩ Fin) → 𝑎 ∈ 𝒫 𝐵) |
| 29 | 28 | adantl 481 |
. . . . . . . 8
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ 𝒫 𝐵) |
| 30 | | elpwi 4607 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵) |
| 31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ⊆ 𝐵) |
| 32 | | f1ocnv 6860 |
. . . . . . . . 9
⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴) |
| 33 | 32 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → ◡𝐹:𝐵–1-1-onto→𝐴) |
| 34 | | f1odm 6852 |
. . . . . . . 8
⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → dom ◡𝐹 = 𝐵) |
| 35 | 33, 34 | syl 17 |
. . . . . . 7
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → dom ◡𝐹 = 𝐵) |
| 36 | 31, 35 | sseqtrrd 4021 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ⊆ dom ◡𝐹) |
| 37 | | fores 6830 |
. . . . . 6
⊢ ((Fun
◡𝐹 ∧ 𝑎 ⊆ dom ◡𝐹) → (◡𝐹 ↾ 𝑎):𝑎–onto→(◡𝐹 “ 𝑎)) |
| 38 | 27, 36, 37 | syl2an2r 685 |
. . . . 5
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (◡𝐹 ↾ 𝑎):𝑎–onto→(◡𝐹 “ 𝑎)) |
| 39 | | fofi 9351 |
. . . . 5
⊢ ((𝑎 ∈ Fin ∧ (◡𝐹 ↾ 𝑎):𝑎–onto→(◡𝐹 “ 𝑎)) → (◡𝐹 “ 𝑎) ∈ Fin) |
| 40 | 25, 38, 39 | syl2anc 584 |
. . . 4
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (◡𝐹 “ 𝑎) ∈ Fin) |
| 41 | | imassrn 6089 |
. . . . . 6
⊢ (◡𝐹 “ 𝑎) ⊆ ran ◡𝐹 |
| 42 | | dfdm4 5906 |
. . . . . . 7
⊢ dom 𝐹 = ran ◡𝐹 |
| 43 | 42, 9 | eqtr3id 2791 |
. . . . . 6
⊢ (𝐹:𝐴–1-1-onto→𝐵 → ran ◡𝐹 = 𝐴) |
| 44 | 41, 43 | sseqtrid 4026 |
. . . . 5
⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 “ 𝑎) ⊆ 𝐴) |
| 45 | 44 | adantr 480 |
. . . 4
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (◡𝐹 “ 𝑎) ⊆ 𝐴) |
| 46 | 40, 45 | elpwd 4606 |
. . 3
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (◡𝐹 “ 𝑎) ∈ 𝒫 𝐴) |
| 47 | 46, 40 | elind 4200 |
. 2
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (◡𝐹 “ 𝑎) ∈ (𝒫 𝐴 ∩ Fin)) |
| 48 | 5, 28 | anim12i 613 |
. . 3
⊢ ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) |
| 49 | 30 | adantl 481 |
. . . . . . 7
⊢ ((𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵) → 𝑎 ⊆ 𝐵) |
| 50 | | foimacnv 6865 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑎 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝑎)) = 𝑎) |
| 51 | 17, 49, 50 | syl2an 596 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (𝐹 “ (◡𝐹 “ 𝑎)) = 𝑎) |
| 52 | 51 | eqcomd 2743 |
. . . . 5
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → 𝑎 = (𝐹 “ (◡𝐹 “ 𝑎))) |
| 53 | | imaeq2 6074 |
. . . . . 6
⊢ (𝑏 = (◡𝐹 “ 𝑎) → (𝐹 “ 𝑏) = (𝐹 “ (◡𝐹 “ 𝑎))) |
| 54 | 53 | eqeq2d 2748 |
. . . . 5
⊢ (𝑏 = (◡𝐹 “ 𝑎) → (𝑎 = (𝐹 “ 𝑏) ↔ 𝑎 = (𝐹 “ (◡𝐹 “ 𝑎)))) |
| 55 | 52, 54 | syl5ibrcom 247 |
. . . 4
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (𝑏 = (◡𝐹 “ 𝑎) → 𝑎 = (𝐹 “ 𝑏))) |
| 56 | | f1of1 6847 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵) |
| 57 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵) → 𝑏 ⊆ 𝐴) |
| 58 | | f1imacnv 6864 |
. . . . . . 7
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑏 ⊆ 𝐴) → (◡𝐹 “ (𝐹 “ 𝑏)) = 𝑏) |
| 59 | 56, 57, 58 | syl2an 596 |
. . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (◡𝐹 “ (𝐹 “ 𝑏)) = 𝑏) |
| 60 | 59 | eqcomd 2743 |
. . . . 5
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → 𝑏 = (◡𝐹 “ (𝐹 “ 𝑏))) |
| 61 | | imaeq2 6074 |
. . . . . 6
⊢ (𝑎 = (𝐹 “ 𝑏) → (◡𝐹 “ 𝑎) = (◡𝐹 “ (𝐹 “ 𝑏))) |
| 62 | 61 | eqeq2d 2748 |
. . . . 5
⊢ (𝑎 = (𝐹 “ 𝑏) → (𝑏 = (◡𝐹 “ 𝑎) ↔ 𝑏 = (◡𝐹 “ (𝐹 “ 𝑏)))) |
| 63 | 60, 62 | syl5ibrcom 247 |
. . . 4
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (𝑎 = (𝐹 “ 𝑏) → 𝑏 = (◡𝐹 “ 𝑎))) |
| 64 | 55, 63 | impbid 212 |
. . 3
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (𝑏 = (◡𝐹 “ 𝑎) ↔ 𝑎 = (𝐹 “ 𝑏))) |
| 65 | 48, 64 | sylan2 593 |
. 2
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑏 = (◡𝐹 “ 𝑎) ↔ 𝑎 = (𝐹 “ 𝑏))) |
| 66 | 1, 23, 47, 65 | f1o2d 7687 |
1
⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹 “ 𝑏)):(𝒫 𝐴 ∩ Fin)–1-1-onto→(𝒫 𝐵 ∩ Fin)) |