Metamath Proof Explorer


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