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	syl5eqr	⊢ ( 𝐹 : 𝐴 –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→ 𝐵 ) → 𝒫 𝐵 ≼ 𝒫 𝐴 )