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⟶ontoB→𝒫B≼𝒫A

Proof

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