Metamath Proof Explorer

Theorem fopwdom

Description: Covering implies injection on power sets. (Contributed by Stefan O'Rear, 6-Nov-2014) (Revised by Mario Carneiro, 24-Jun-2015) (Revised by AV, 18-Sep-2021)

Ref Expression
Assertion fopwdom ⊢ F ∈ V ∧ F : A ⟶ onto B → 𝒫 B ≼ 𝒫 A

Proof

Step Hyp Ref Expression
1 imassrn ⊢ F -1 a ⊆ ran ⁡ F -1
2 dfdm4 ⊢ dom ⁡ F = ran ⁡ F -1
3 fof ⊢ F : A ⟶ onto B → F : A ⟶ B
4 3 fdmd ⊢ F : A ⟶ onto B → dom ⁡ F = A
5 2 4 syl5eqr ⊢ F : A ⟶ onto B → ran ⁡ F -1 = A
6 1 5 sseqtrid ⊢ F : A ⟶ onto B → F -1 a ⊆ A
7 6 adantl ⊢ F ∈ V ∧ F : A ⟶ onto B → F -1 a ⊆ A
8 cnvexg ⊢ F ∈ V → F -1 ∈ V
9 8 adantr ⊢ F ∈ V ∧ F : A ⟶ onto B → F -1 ∈ V
10 imaexg ⊢ F -1 ∈ V → F -1 a ∈ V
11 elpwg ⊢ F -1 a ∈ V → F -1 a ∈ 𝒫 A ↔ F -1 a ⊆ A
12 9 10 11 3syl ⊢ F ∈ V ∧ F : A ⟶ onto B → F -1 a ∈ 𝒫 A ↔ F -1 a ⊆ A
13 7 12 mpbird ⊢ F ∈ V ∧ F : A ⟶ onto B → F -1 a ∈ 𝒫 A
14 13 a1d ⊢ F ∈ V ∧ F : A ⟶ onto B → a ∈ 𝒫 B → F -1 a ∈ 𝒫 A
15 imaeq2 ⊢ F -1 a = F -1 b → F F -1 a = F F -1 b
16 15 adantl ⊢ F ∈ V ∧ F : A ⟶ onto B ∧ a ∈ 𝒫 B ∧ b ∈ 𝒫 B ∧ F -1 a = F -1 b → F F -1 a = F F -1 b
17 simpllr ⊢ F ∈ V ∧ F : A ⟶ onto B ∧ a ∈ 𝒫 B ∧ b ∈ 𝒫 B ∧ F -1 a = F -1 b → F : A ⟶ onto B
18 simplrl ⊢ F ∈ V ∧ F : A ⟶ onto B ∧ a ∈ 𝒫 B ∧ b ∈ 𝒫 B ∧ F -1 a = F -1 b → a ∈ 𝒫 B
19 18 elpwid ⊢ F ∈ V ∧ F : A ⟶ onto B ∧ a ∈ 𝒫 B ∧ b ∈ 𝒫 B ∧ F -1 a = F -1 b → a ⊆ B
20 foimacnv ⊢ F : A ⟶ onto B ∧ a ⊆ B → F F -1 a = a
21 17 19 20 syl2anc ⊢ F ∈ V ∧ F : A ⟶ onto B ∧ a ∈ 𝒫 B ∧ b ∈ 𝒫 B ∧ F -1 a = F -1 b → F F -1 a = a
22 simplrr ⊢ F ∈ V ∧ F : A ⟶ onto B ∧ a ∈ 𝒫 B ∧ b ∈ 𝒫 B ∧ F -1 a = F -1 b → b ∈ 𝒫 B
23 22 elpwid ⊢ F ∈ V ∧ F : A ⟶ onto B ∧ a ∈ 𝒫 B ∧ b ∈ 𝒫 B ∧ F -1 a = F -1 b → b ⊆ B
24 foimacnv ⊢ F : A ⟶ onto B ∧ b ⊆ B → F F -1 b = b
25 17 23 24 syl2anc ⊢ F ∈ V ∧ F : A ⟶ onto B ∧ a ∈ 𝒫 B ∧ b ∈ 𝒫 B ∧ F -1 a = F -1 b → F F -1 b = b
26 16 21 25 3eqtr3d ⊢ F ∈ V ∧ F : A ⟶ onto B ∧ a ∈ 𝒫 B ∧ b ∈ 𝒫 B ∧ F -1 a = F -1 b → a = b
27 26 ex ⊢ F ∈ V ∧ F : A ⟶ onto B ∧ a ∈ 𝒫 B ∧ b ∈ 𝒫 B → F -1 a = F -1 b → a = b
28 imaeq2 ⊢ a = b → F -1 a = F -1 b
29 27 28 impbid1 ⊢ F ∈ V ∧ F : A ⟶ onto B ∧ a ∈ 𝒫 B ∧ b ∈ 𝒫 B → F -1 a = F -1 b ↔ a = b
30 29 ex ⊢ F ∈ V ∧ F : A ⟶ onto B → a ∈ 𝒫 B ∧ b ∈ 𝒫 B → F -1 a = F -1 b ↔ a = b
31 rnexg ⊢ F ∈ V → ran ⁡ F ∈ V
32 forn ⊢ F : A ⟶ onto B → ran ⁡ F = B
33 32 eleq1d ⊢ F : A ⟶ onto B → ran ⁡ F ∈ V ↔ B ∈ V
34 31 33 syl5ibcom ⊢ F ∈ V → F : A ⟶ onto B → B ∈ V
35 34 imp ⊢ F ∈ V ∧ F : A ⟶ onto B → B ∈ V
36 35 pwexd ⊢ F ∈ V ∧ F : A ⟶ onto B → 𝒫 B ∈ V
37 dmfex ⊢ F ∈ V ∧ F : A ⟶ B → A ∈ V
38 3 37 sylan2 ⊢ F ∈ V ∧ F : A ⟶ onto B → A ∈ V
39 38 pwexd ⊢ F ∈ V ∧ F : A ⟶ onto B → 𝒫 A ∈ V
40 14 30 36 39 dom3d ⊢ F ∈ V ∧ F : A ⟶ onto B → 𝒫 B ≼ 𝒫 A