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 ( ( 𝐹𝑉𝐹 : 𝐴onto𝐵 ) → 𝒫 𝐵 ≼ 𝒫 𝐴 )

Proof

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