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 ⊢ M = x ∈ A ⟼ F x
mptcnfimad.f ⊢ φ → F : V ⟶ 1-1 onto W
mptcnfimad.a ⊢ φ → A ⊆ 𝒫 V
mptcnfimad.r ⊢ φ → ran ⁡ M ⊆ 𝒫 W
mptcnfimad.v ⊢ φ → V ∈ U
Assertion mptcnfimad ⊢ φ → M -1 = y ∈ ran ⁡ M ⟼ F -1 y

Proof

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