Metamath Proof Explorer

Theorem isotr

Description: Composition (transitive) law for isomorphism. Proposition 6.30(3) of TakeutiZaring p. 33. (Contributed by NM, 27-Apr-2004) (Proof shortened by Mario Carneiro, 5-Dec-2016)

Ref Expression
Assertion isotr ⊢HIsomR,SAB∧GIsomS,TBC→G∘HIsomR,TAC

Proof

Step Hyp Ref Expression
1 simpl ⊢G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w→G:B⟶1-1 ontoC
2 simpl ⊢H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y→H:A⟶1-1 ontoB
3 f1oco ⊢G:B⟶1-1 ontoC∧H:A⟶1-1 ontoB→G∘H:A⟶1-1 ontoC
4 1 2 3 syl2anr ⊢H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w→G∘H:A⟶1-1 ontoC
5 f1of ⊢H:A⟶1-1 ontoB→H:A⟶B
6 5 ad2antrr ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w∧x∈A∧y∈A→H:A⟶B
7 simprl ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w∧x∈A∧y∈A→x∈A
8 6 7 ffvelcdmd ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w∧x∈A∧y∈A→H⁡x∈B
9 simprr ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w∧x∈A∧y∈A→y∈A
10 6 9 ffvelcdmd ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w∧x∈A∧y∈A→H⁡y∈B
11 simplrr ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w∧x∈A∧y∈A→∀z∈B∀w∈BzSw↔G⁡zTG⁡w
12 breq1 ⊢z=H⁡x→zSw↔H⁡xSw
13 fveq2 ⊢z=H⁡x→G⁡z=G⁡H⁡x
14 13 breq1d ⊢z=H⁡x→G⁡zTG⁡w↔G⁡H⁡xTG⁡w
15 12 14 bibi12d ⊢z=H⁡x→zSw↔G⁡zTG⁡w↔H⁡xSw↔G⁡H⁡xTG⁡w
16 breq2 ⊢w=H⁡y→H⁡xSw↔H⁡xSH⁡y
17 fveq2 ⊢w=H⁡y→G⁡w=G⁡H⁡y
18 17 breq2d ⊢w=H⁡y→G⁡H⁡xTG⁡w↔G⁡H⁡xTG⁡H⁡y
19 16 18 bibi12d ⊢w=H⁡y→H⁡xSw↔G⁡H⁡xTG⁡w↔H⁡xSH⁡y↔G⁡H⁡xTG⁡H⁡y
20 15 19 rspc2va ⊢H⁡x∈B∧H⁡y∈B∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w→H⁡xSH⁡y↔G⁡H⁡xTG⁡H⁡y
21 8 10 11 20 syl21anc ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w∧x∈A∧y∈A→H⁡xSH⁡y↔G⁡H⁡xTG⁡H⁡y
22 fvco3 ⊢H:A⟶B∧x∈A→G∘H⁡x=G⁡H⁡x
23 6 7 22 syl2anc ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w∧x∈A∧y∈A→G∘H⁡x=G⁡H⁡x
24 fvco3 ⊢H:A⟶B∧y∈A→G∘H⁡y=G⁡H⁡y
25 6 9 24 syl2anc ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w∧x∈A∧y∈A→G∘H⁡y=G⁡H⁡y
26 23 25 breq12d ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w∧x∈A∧y∈A→G∘H⁡xTG∘H⁡y↔G⁡H⁡xTG⁡H⁡y
27 21 26 bitr4d ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w∧x∈A∧y∈A→H⁡xSH⁡y↔G∘H⁡xTG∘H⁡y
28 27 bibi2d ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w∧x∈A∧y∈A→xRy↔H⁡xSH⁡y↔xRy↔G∘H⁡xTG∘H⁡y
29 28 2ralbidva ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w→∀x∈A∀y∈AxRy↔H⁡xSH⁡y↔∀x∈A∀y∈AxRy↔G∘H⁡xTG∘H⁡y
30 29 biimpd ⊢H:A⟶1-1 ontoB∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w→∀x∈A∀y∈AxRy↔H⁡xSH⁡y→∀x∈A∀y∈AxRy↔G∘H⁡xTG∘H⁡y
31 30 impancom ⊢H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y→G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w→∀x∈A∀y∈AxRy↔G∘H⁡xTG∘H⁡y
32 31 imp ⊢H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w→∀x∈A∀y∈AxRy↔G∘H⁡xTG∘H⁡y
33 4 32 jca ⊢H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w→G∘H:A⟶1-1 ontoC∧∀x∈A∀y∈AxRy↔G∘H⁡xTG∘H⁡y
34 df-isom ⊢HIsomR,SAB↔H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y
35 df-isom ⊢GIsomS,TBC↔G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w
36 34 35 anbi12i ⊢HIsomR,SAB∧GIsomS,TBC↔H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y∧G:B⟶1-1 ontoC∧∀z∈B∀w∈BzSw↔G⁡zTG⁡w
37 df-isom ⊢G∘HIsomR,TAC↔G∘H:A⟶1-1 ontoC∧∀x∈A∀y∈AxRy↔G∘H⁡xTG∘H⁡y
38 33 36 37 3imtr4i ⊢HIsomR,SAB∧GIsomS,TBC→G∘HIsomR,TAC