This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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→ 𝐵 ) → 𝒫 𝐵 ≼ 𝒫 𝐴 )