Metamath Proof Explorer

Theorem imaf1homlem

Description: Lemma for imaf1hom and other theorems. (Contributed by Zhi Wang, 7-Nov-2025)

Ref Expression
Hypotheses imaf1hom.s ⊢ S = F A
imaf1hom.1 ⊢ φ → F : B ⟶ 1-1 C
imaf1hom.x ⊢ φ → X ∈ S
Assertion imaf1homlem ⊢ φ → F -1 ⁡ X = F -1 X ∧ F ⁡ F -1 ⁡ X = X ∧ F -1 ⁡ X ∈ B

Proof

Step Hyp Ref Expression
1 imaf1hom.s ⊢ S = F A
2 imaf1hom.1 ⊢ φ → F : B ⟶ 1-1 C
3 imaf1hom.x ⊢ φ → X ∈ S
4 f1f1orn ⊢ F : B ⟶ 1-1 C → F : B ⟶ 1-1 onto ran ⁡ F
5 2 4 syl ⊢ φ → F : B ⟶ 1-1 onto ran ⁡ F
6 dff1o4 ⊢ F : B ⟶ 1-1 onto ran ⁡ F ↔ F Fn B ∧ F -1 Fn ran ⁡ F
7 6 simprbi ⊢ F : B ⟶ 1-1 onto ran ⁡ F → F -1 Fn ran ⁡ F
8 5 7 syl ⊢ φ → F -1 Fn ran ⁡ F
9 imassrn ⊢ F A ⊆ ran ⁡ F
10 3 1 eleqtrdi ⊢ φ → X ∈ F A
11 9 10 sselid ⊢ φ → X ∈ ran ⁡ F
12 fnsnfv ⊢ F -1 Fn ran ⁡ F ∧ X ∈ ran ⁡ F → F -1 ⁡ X = F -1 X
13 8 11 12 syl2anc ⊢ φ → F -1 ⁡ X = F -1 X
14 f1ocnvfv2 ⊢ F : B ⟶ 1-1 onto ran ⁡ F ∧ X ∈ ran ⁡ F → F ⁡ F -1 ⁡ X = X
15 5 11 14 syl2anc ⊢ φ → F ⁡ F -1 ⁡ X = X
16 f1ocnvdm ⊢ F : B ⟶ 1-1 onto ran ⁡ F ∧ X ∈ ran ⁡ F → F -1 ⁡ X ∈ B
17 5 11 16 syl2anc ⊢ φ → F -1 ⁡ X ∈ B
18 13 15 17 3jca ⊢ φ → F -1 ⁡ X = F -1 X ∧ F ⁡ F -1 ⁡ X = X ∧ F -1 ⁡ X ∈ B