f1opw2

Description: A one-to-one mapping induces a one-to-one mapping on power sets. This version of f1opw avoids the Axiom of Replacement. (Contributed by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	f1opw2.1	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
	f1opw2.2	⊢ ( 𝜑 → ( ^◡ 𝐹 “ 𝑎 ) ∈ V )
	f1opw2.3	⊢ ( 𝜑 → ( 𝐹 “ 𝑏 ) ∈ V )
Assertion	f1opw2	⊢ ( 𝜑 → ( 𝑏 ∈ 𝒫 𝐴 ↦ ( 𝐹 “ 𝑏 ) ) : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		f1opw2.1	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
2		f1opw2.2	⊢ ( 𝜑 → ( ^◡ 𝐹 “ 𝑎 ) ∈ V )
3		f1opw2.3	⊢ ( 𝜑 → ( 𝐹 “ 𝑏 ) ∈ V )
4		eqid	⊢ ( 𝑏 ∈ 𝒫 𝐴 ↦ ( 𝐹 “ 𝑏 ) ) = ( 𝑏 ∈ 𝒫 𝐴 ↦ ( 𝐹 “ 𝑏 ) )
5		imassrn	⊢ ( 𝐹 “ 𝑏 ) ⊆ ran 𝐹
6		f1ofo	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –onto→ 𝐵 )
7	1 6	syl	⊢ ( 𝜑 → 𝐹 : 𝐴 –onto→ 𝐵 )
8		forn	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
9	7 8	syl	⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
10	5 9	sseqtrid	⊢ ( 𝜑 → ( 𝐹 “ 𝑏 ) ⊆ 𝐵 )
11	3 10	elpwd	⊢ ( 𝜑 → ( 𝐹 “ 𝑏 ) ∈ 𝒫 𝐵 )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝒫 𝐴 ) → ( 𝐹 “ 𝑏 ) ∈ 𝒫 𝐵 )
13		imassrn	⊢ ( ^◡ 𝐹 “ 𝑎 ) ⊆ ran ^◡ 𝐹
14		dfdm4	⊢ dom 𝐹 = ran ^◡ 𝐹
15		f1odm	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → dom 𝐹 = 𝐴 )
16	1 15	syl	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
17	14 16	eqtr3id	⊢ ( 𝜑 → ran ^◡ 𝐹 = 𝐴 )
18	13 17	sseqtrid	⊢ ( 𝜑 → ( ^◡ 𝐹 “ 𝑎 ) ⊆ 𝐴 )
19	2 18	elpwd	⊢ ( 𝜑 → ( ^◡ 𝐹 “ 𝑎 ) ∈ 𝒫 𝐴 )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐵 ) → ( ^◡ 𝐹 “ 𝑎 ) ∈ 𝒫 𝐴 )
21		elpwi	⊢ ( 𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵 )
22	21	adantl	⊢ ( ( 𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵 ) → 𝑎 ⊆ 𝐵 )
23		foimacnv	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑎 ⊆ 𝐵 ) → ( 𝐹 “ ( ^◡ 𝐹 “ 𝑎 ) ) = 𝑎 )
24	7 22 23	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵 ) ) → ( 𝐹 “ ( ^◡ 𝐹 “ 𝑎 ) ) = 𝑎 )
25	24	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵 ) ) → 𝑎 = ( 𝐹 “ ( ^◡ 𝐹 “ 𝑎 ) ) )
26		imaeq2	⊢ ( 𝑏 = ( ^◡ 𝐹 “ 𝑎 ) → ( 𝐹 “ 𝑏 ) = ( 𝐹 “ ( ^◡ 𝐹 “ 𝑎 ) ) )
27	26	eqeq2d	⊢ ( 𝑏 = ( ^◡ 𝐹 “ 𝑎 ) → ( 𝑎 = ( 𝐹 “ 𝑏 ) ↔ 𝑎 = ( 𝐹 “ ( ^◡ 𝐹 “ 𝑎 ) ) ) )
28	25 27	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵 ) ) → ( 𝑏 = ( ^◡ 𝐹 “ 𝑎 ) → 𝑎 = ( 𝐹 “ 𝑏 ) ) )
29		f1of1	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –1-1→ 𝐵 )
30	1 29	syl	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )
31		elpwi	⊢ ( 𝑏 ∈ 𝒫 𝐴 → 𝑏 ⊆ 𝐴 )
32	31	adantr	⊢ ( ( 𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵 ) → 𝑏 ⊆ 𝐴 )
33		f1imacnv	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑏 ⊆ 𝐴 ) → ( ^◡ 𝐹 “ ( 𝐹 “ 𝑏 ) ) = 𝑏 )
34	30 32 33	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵 ) ) → ( ^◡ 𝐹 “ ( 𝐹 “ 𝑏 ) ) = 𝑏 )
35	34	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵 ) ) → 𝑏 = ( ^◡ 𝐹 “ ( 𝐹 “ 𝑏 ) ) )
36		imaeq2	⊢ ( 𝑎 = ( 𝐹 “ 𝑏 ) → ( ^◡ 𝐹 “ 𝑎 ) = ( ^◡ 𝐹 “ ( 𝐹 “ 𝑏 ) ) )
37	36	eqeq2d	⊢ ( 𝑎 = ( 𝐹 “ 𝑏 ) → ( 𝑏 = ( ^◡ 𝐹 “ 𝑎 ) ↔ 𝑏 = ( ^◡ 𝐹 “ ( 𝐹 “ 𝑏 ) ) ) )
38	35 37	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵 ) ) → ( 𝑎 = ( 𝐹 “ 𝑏 ) → 𝑏 = ( ^◡ 𝐹 “ 𝑎 ) ) )
39	28 38	impbid	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵 ) ) → ( 𝑏 = ( ^◡ 𝐹 “ 𝑎 ) ↔ 𝑎 = ( 𝐹 “ 𝑏 ) ) )
40	4 12 20 39	f1o2d	⊢ ( 𝜑 → ( 𝑏 ∈ 𝒫 𝐴 ↦ ( 𝐹 “ 𝑏 ) ) : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐵 )

Metamath Proof Explorer

Theorem f1opw2

Proof