Metamath Proof Explorer

Theorem mptcnfimad

Description: The converse of a mapping of subsets to their image of a bijection. (Contributed by AV, 23-Apr-2025)

Ref Expression
Hypotheses mptcnfimad.m ⊢ 𝑀 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 “ 𝑥 ) )
mptcnfimad.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
mptcnfimad.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝒫 𝑉 )
mptcnfimad.r ⊢ ( 𝜑 → ran 𝑀 ⊆ 𝒫 𝑊 )
mptcnfimad.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
Assertion mptcnfimad ( 𝜑 → ◡ 𝑀 = ( 𝑦 ∈ ran 𝑀 ↦ ( ◡ 𝐹 “ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 mptcnfimad.m ⊢ 𝑀 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 “ 𝑥 ) )
2 mptcnfimad.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
3 mptcnfimad.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝒫 𝑉 )
4 mptcnfimad.r ⊢ ( 𝜑 → ran 𝑀 ⊆ 𝒫 𝑊 )
5 mptcnfimad.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
6 1 cnveqi ⊢ ◡ 𝑀 = ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 “ 𝑥 ) )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
8 f1of ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 : 𝑉 ⟶ 𝑊 )
9 2 8 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶ 𝑊 )
10 9 5 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
11 10 imaexd ⊢ ( 𝜑 → ( 𝐹 “ 𝑥 ) ∈ V )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 “ 𝑥 ) ∈ V )
13 1 7 12 elrnmpt1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 “ 𝑥 ) ∈ ran 𝑀 )
14 f1of1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 : 𝑉 –1-1→ 𝑊 )
15 2 14 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1→ 𝑊 )
16 ssel ⊢ ( 𝐴 ⊆ 𝒫 𝑉 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝑉 ) )
17 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑉 → 𝑥 ⊆ 𝑉 )
18 16 17 syl6 ⊢ ( 𝐴 ⊆ 𝒫 𝑉 → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝑉 ) )
19 3 18 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝑉 ) )
20 19 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ⊆ 𝑉 )
21 f1imacnv ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ 𝑥 ⊆ 𝑉 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) = 𝑥 )
22 21 eqcomd ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ 𝑥 ⊆ 𝑉 ) → 𝑥 = ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) )
23 15 20 22 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) )
24 13 23 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 “ 𝑥 ) ∈ ran 𝑀 ∧ 𝑥 = ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) ) )
25 eleq1 ⊢ ( 𝑦 = ( 𝐹 “ 𝑥 ) → ( 𝑦 ∈ ran 𝑀 ↔ ( 𝐹 “ 𝑥 ) ∈ ran 𝑀 ) )
26 imaeq2 ⊢ ( 𝑦 = ( 𝐹 “ 𝑥 ) → ( ◡ 𝐹 “ 𝑦 ) = ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) )
27 26 eqeq2d ⊢ ( 𝑦 = ( 𝐹 “ 𝑥 ) → ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) ↔ 𝑥 = ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) ) )
28 25 27 anbi12d ⊢ ( 𝑦 = ( 𝐹 “ 𝑥 ) → ( ( 𝑦 ∈ ran 𝑀 ∧ 𝑥 = ( ◡ 𝐹 “ 𝑦 ) ) ↔ ( ( 𝐹 “ 𝑥 ) ∈ ran 𝑀 ∧ 𝑥 = ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) ) ) )
29 24 28 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 “ 𝑥 ) → ( 𝑦 ∈ ran 𝑀 ∧ 𝑥 = ( ◡ 𝐹 “ 𝑦 ) ) ) )
30 29 expimpd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 “ 𝑥 ) ) → ( 𝑦 ∈ ran 𝑀 ∧ 𝑥 = ( ◡ 𝐹 “ 𝑦 ) ) ) )
31 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 “ 𝑥 ) ∈ V )
32 1 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 “ 𝑥 ) ∈ V → 𝑀 Fn 𝐴 )
33 31 32 syl ⊢ ( 𝜑 → 𝑀 Fn 𝐴 )
34 fvelrnb ⊢ ( 𝑀 Fn 𝐴 → ( 𝑦 ∈ ran 𝑀 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) = 𝑦 ) )
35 33 34 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝑀 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) = 𝑦 ) )
36 imaeq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑧 ) )
37 36 cbvmptv ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 “ 𝑥 ) ) = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 “ 𝑧 ) )
38 1 37 eqtri ⊢ 𝑀 = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 “ 𝑧 ) )
39 38 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 “ 𝑧 ) ) )
40 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 = 𝑥 ) → 𝑧 = 𝑥 )
41 40 imaeq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 = 𝑥 ) → ( 𝐹 “ 𝑧 ) = ( 𝐹 “ 𝑥 ) )
42 39 41 7 12 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑥 ) = ( 𝐹 “ 𝑥 ) )
43 42 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑀 ‘ 𝑥 ) = 𝑦 ↔ ( 𝐹 “ 𝑥 ) = 𝑦 ) )
44 26 eqcoms ⊢ ( ( 𝐹 “ 𝑥 ) = 𝑦 → ( ◡ 𝐹 “ 𝑦 ) = ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) )
45 44 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 “ 𝑥 ) = 𝑦 ) → ( ◡ 𝐹 “ 𝑦 ) = ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) )
46 15 20 21 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) = 𝑥 )
47 46 7 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) ∈ 𝐴 )
48 47 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 “ 𝑥 ) = 𝑦 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) ∈ 𝐴 )
49 45 48 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 “ 𝑥 ) = 𝑦 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐴 )
50 49 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 “ 𝑥 ) = 𝑦 → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐴 ) )
51 43 50 sylbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑀 ‘ 𝑥 ) = 𝑦 → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐴 ) )
52 51 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) = 𝑦 → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐴 ) )
53 35 52 sylbid ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝑀 → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐴 ) )
54 53 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑀 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐴 )
55 f1ofo ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 : 𝑉 –onto→ 𝑊 )
56 2 55 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝑊 )
57 ssel ⊢ ( ran 𝑀 ⊆ 𝒫 𝑊 → ( 𝑦 ∈ ran 𝑀 → 𝑦 ∈ 𝒫 𝑊 ) )
58 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑊 → 𝑦 ⊆ 𝑊 )
59 57 58 syl6 ⊢ ( ran 𝑀 ⊆ 𝒫 𝑊 → ( 𝑦 ∈ ran 𝑀 → 𝑦 ⊆ 𝑊 ) )
60 4 59 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝑀 → 𝑦 ⊆ 𝑊 ) )
61 60 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑀 ) → 𝑦 ⊆ 𝑊 )
62 foimacnv ⊢ ( ( 𝐹 : 𝑉 –onto→ 𝑊 ∧ 𝑦 ⊆ 𝑊 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 )
63 56 61 62 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑀 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 )
64 63 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑀 ) → 𝑦 = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) )
65 54 64 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑀 ) → ( ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐴 ∧ 𝑦 = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) )
66 eleq1 ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝑥 ∈ 𝐴 ↔ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐴 ) )
67 imaeq2 ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) )
68 67 eqeq2d ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝑦 = ( 𝐹 “ 𝑥 ) ↔ 𝑦 = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) )
69 66 68 anbi12d ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 “ 𝑥 ) ) ↔ ( ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐴 ∧ 𝑦 = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) ) )
70 65 69 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑀 ) → ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 “ 𝑥 ) ) ) )
71 70 expimpd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ran 𝑀 ∧ 𝑥 = ( ◡ 𝐹 “ 𝑦 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 “ 𝑥 ) ) ) )
72 30 71 impbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 “ 𝑥 ) ) ↔ ( 𝑦 ∈ ran 𝑀 ∧ 𝑥 = ( ◡ 𝐹 “ 𝑦 ) ) ) )
73 72 mptcnv ⊢ ( 𝜑 → ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 “ 𝑥 ) ) = ( 𝑦 ∈ ran 𝑀 ↦ ( ◡ 𝐹 “ 𝑦 ) ) )
74 6 73 eqtrid ⊢ ( 𝜑 → ◡ 𝑀 = ( 𝑦 ∈ ran 𝑀 ↦ ( ◡ 𝐹 “ 𝑦 ) ) )