Metamath Proof Explorer

Theorem 3f1oss2

Description: The composition of three bijections as bijection from the image of the converse of the domain onto the image of the converse of the range of the middle bijection. (Contributed by AV, 15-Aug-2025)

Ref Expression
Assertion 3f1oss2 ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ H : E ⟶ 1-1 onto I ∧ C ⊆ B ∧ D ⊆ I → H -1 ∘ G ∘ F : F -1 C ⟶ 1-1 onto H -1 D

Proof

Step Hyp Ref Expression
1 f1ocnv ⊢ F : A ⟶ 1-1 onto B → F -1 : B ⟶ 1-1 onto A
2 id ⊢ G : C ⟶ 1-1 onto D → G : C ⟶ 1-1 onto D
3 f1ocnv ⊢ H : E ⟶ 1-1 onto I → H -1 : I ⟶ 1-1 onto E
4 3f1oss1 ⊢ F -1 : B ⟶ 1-1 onto A ∧ G : C ⟶ 1-1 onto D ∧ H -1 : I ⟶ 1-1 onto E ∧ C ⊆ B ∧ D ⊆ I → H -1 ∘ G ∘ F -1 -1 : F -1 C ⟶ 1-1 onto H -1 D
5 1 2 3 4 syl3anl ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ H : E ⟶ 1-1 onto I ∧ C ⊆ B ∧ D ⊆ I → H -1 ∘ G ∘ F -1 -1 : F -1 C ⟶ 1-1 onto H -1 D
6 f1orel ⊢ F : A ⟶ 1-1 onto B → Rel ⁡ F
7 dfrel2 ⊢ Rel ⁡ F ↔ F -1 -1 = F
8 7 biimpi ⊢ Rel ⁡ F → F -1 -1 = F
9 8 eqcomd ⊢ Rel ⁡ F → F = F -1 -1
10 9 coeq2d ⊢ Rel ⁡ F → H -1 ∘ G ∘ F = H -1 ∘ G ∘ F -1 -1
11 10 f1oeq1d ⊢ Rel ⁡ F → H -1 ∘ G ∘ F : F -1 C ⟶ 1-1 onto H -1 D ↔ H -1 ∘ G ∘ F -1 -1 : F -1 C ⟶ 1-1 onto H -1 D
12 6 11 syl ⊢ F : A ⟶ 1-1 onto B → H -1 ∘ G ∘ F : F -1 C ⟶ 1-1 onto H -1 D ↔ H -1 ∘ G ∘ F -1 -1 : F -1 C ⟶ 1-1 onto H -1 D
13 12 3ad2ant1 ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ H : E ⟶ 1-1 onto I → H -1 ∘ G ∘ F : F -1 C ⟶ 1-1 onto H -1 D ↔ H -1 ∘ G ∘ F -1 -1 : F -1 C ⟶ 1-1 onto H -1 D
14 13 adantr ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ H : E ⟶ 1-1 onto I ∧ C ⊆ B ∧ D ⊆ I → H -1 ∘ G ∘ F : F -1 C ⟶ 1-1 onto H -1 D ↔ H -1 ∘ G ∘ F -1 -1 : F -1 C ⟶ 1-1 onto H -1 D
15 5 14 mpbird ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ H : E ⟶ 1-1 onto I ∧ C ⊆ B ∧ D ⊆ I → H -1 ∘ G ∘ F : F -1 C ⟶ 1-1 onto H -1 D