| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | imassrn 6089 | . . . . . 6
⊢ (◡𝐹 “ 𝑎) ⊆ ran ◡𝐹 | 
| 2 |  | dfdm4 5906 | . . . . . . 7
⊢ dom 𝐹 = ran ◡𝐹 | 
| 3 |  | fof 6820 | . . . . . . . 8
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | 
| 4 | 3 | fdmd 6746 | . . . . . . 7
⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴) | 
| 5 | 2, 4 | eqtr3id 2791 | . . . . . 6
⊢ (𝐹:𝐴–onto→𝐵 → ran ◡𝐹 = 𝐴) | 
| 6 | 1, 5 | sseqtrid 4026 | . . . . 5
⊢ (𝐹:𝐴–onto→𝐵 → (◡𝐹 “ 𝑎) ⊆ 𝐴) | 
| 7 | 6 | adantl 481 | . . . 4
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → (◡𝐹 “ 𝑎) ⊆ 𝐴) | 
| 8 |  | cnvexg 7946 | . . . . . 6
⊢ (𝐹 ∈ 𝑉 → ◡𝐹 ∈ V) | 
| 9 | 8 | adantr 480 | . . . . 5
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → ◡𝐹 ∈ V) | 
| 10 |  | imaexg 7935 | . . . . 5
⊢ (◡𝐹 ∈ V → (◡𝐹 “ 𝑎) ∈ V) | 
| 11 |  | elpwg 4603 | . . . . 5
⊢ ((◡𝐹 “ 𝑎) ∈ V → ((◡𝐹 “ 𝑎) ∈ 𝒫 𝐴 ↔ (◡𝐹 “ 𝑎) ⊆ 𝐴)) | 
| 12 | 9, 10, 11 | 3syl 18 | . . . 4
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → ((◡𝐹 “ 𝑎) ∈ 𝒫 𝐴 ↔ (◡𝐹 “ 𝑎) ⊆ 𝐴)) | 
| 13 | 7, 12 | mpbird 257 | . . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → (◡𝐹 “ 𝑎) ∈ 𝒫 𝐴) | 
| 14 | 13 | a1d 25 | . 2
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → (𝑎 ∈ 𝒫 𝐵 → (◡𝐹 “ 𝑎) ∈ 𝒫 𝐴)) | 
| 15 |  | imaeq2 6074 | . . . . . . 7
⊢ ((◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏) → (𝐹 “ (◡𝐹 “ 𝑎)) = (𝐹 “ (◡𝐹 “ 𝑏))) | 
| 16 | 15 | adantl 481 | . . . . . 6
⊢ ((((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) ∧ (𝑎 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ 𝒫 𝐵)) ∧ (◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏)) → (𝐹 “ (◡𝐹 “ 𝑎)) = (𝐹 “ (◡𝐹 “ 𝑏))) | 
| 17 |  | simpllr 776 | . . . . . . 7
⊢ ((((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) ∧ (𝑎 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ 𝒫 𝐵)) ∧ (◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏)) → 𝐹:𝐴–onto→𝐵) | 
| 18 |  | simplrl 777 | . . . . . . . 8
⊢ ((((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) ∧ (𝑎 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ 𝒫 𝐵)) ∧ (◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏)) → 𝑎 ∈ 𝒫 𝐵) | 
| 19 | 18 | elpwid 4609 | . . . . . . 7
⊢ ((((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) ∧ (𝑎 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ 𝒫 𝐵)) ∧ (◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏)) → 𝑎 ⊆ 𝐵) | 
| 20 |  | foimacnv 6865 | . . . . . . 7
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑎 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝑎)) = 𝑎) | 
| 21 | 17, 19, 20 | syl2anc 584 | . . . . . 6
⊢ ((((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) ∧ (𝑎 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ 𝒫 𝐵)) ∧ (◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏)) → (𝐹 “ (◡𝐹 “ 𝑎)) = 𝑎) | 
| 22 |  | simplrr 778 | . . . . . . . 8
⊢ ((((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) ∧ (𝑎 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ 𝒫 𝐵)) ∧ (◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏)) → 𝑏 ∈ 𝒫 𝐵) | 
| 23 | 22 | elpwid 4609 | . . . . . . 7
⊢ ((((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) ∧ (𝑎 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ 𝒫 𝐵)) ∧ (◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏)) → 𝑏 ⊆ 𝐵) | 
| 24 |  | foimacnv 6865 | . . . . . . 7
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑏 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝑏)) = 𝑏) | 
| 25 | 17, 23, 24 | syl2anc 584 | . . . . . 6
⊢ ((((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) ∧ (𝑎 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ 𝒫 𝐵)) ∧ (◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏)) → (𝐹 “ (◡𝐹 “ 𝑏)) = 𝑏) | 
| 26 | 16, 21, 25 | 3eqtr3d 2785 | . . . . 5
⊢ ((((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) ∧ (𝑎 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ 𝒫 𝐵)) ∧ (◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏)) → 𝑎 = 𝑏) | 
| 27 | 26 | ex 412 | . . . 4
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) ∧ (𝑎 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ 𝒫 𝐵)) → ((◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏) → 𝑎 = 𝑏)) | 
| 28 |  | imaeq2 6074 | . . . 4
⊢ (𝑎 = 𝑏 → (◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏)) | 
| 29 | 27, 28 | impbid1 225 | . . 3
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) ∧ (𝑎 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ 𝒫 𝐵)) → ((◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏) ↔ 𝑎 = 𝑏)) | 
| 30 | 29 | ex 412 | . 2
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → ((𝑎 ∈ 𝒫 𝐵 ∧ 𝑏 ∈ 𝒫 𝐵) → ((◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑏) ↔ 𝑎 = 𝑏))) | 
| 31 |  | rnexg 7924 | . . . . 5
⊢ (𝐹 ∈ 𝑉 → ran 𝐹 ∈ V) | 
| 32 |  | forn 6823 | . . . . . 6
⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) | 
| 33 | 32 | eleq1d 2826 | . . . . 5
⊢ (𝐹:𝐴–onto→𝐵 → (ran 𝐹 ∈ V ↔ 𝐵 ∈ V)) | 
| 34 | 31, 33 | syl5ibcom 245 | . . . 4
⊢ (𝐹 ∈ 𝑉 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V)) | 
| 35 | 34 | imp 406 | . . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ V) | 
| 36 | 35 | pwexd 5379 | . 2
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → 𝒫 𝐵 ∈ V) | 
| 37 |  | dmfex 7927 | . . . 4
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴⟶𝐵) → 𝐴 ∈ V) | 
| 38 | 3, 37 | sylan2 593 | . . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → 𝐴 ∈ V) | 
| 39 | 38 | pwexd 5379 | . 2
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → 𝒫 𝐴 ∈ V) | 
| 40 | 14, 30, 36, 39 | dom3d 9034 | 1
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → 𝒫 𝐵 ≼ 𝒫 𝐴) |