Metamath Proof Explorer

Theorem 3f1oss1

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

Ref Expression
Assertion 3f1oss1 
|- ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( ( H o. G ) o. `' F ) : ( F " C ) -1-1-onto-> ( H " D ) )

Proof

Step Hyp Ref Expression
1 f1ocnv 
 |-  ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )
2 f1of1 
 |-  ( `' F : B -1-1-onto-> A -> `' F : B -1-1-> A )
3 1 2 syl 
 |-  ( F : A -1-1-onto-> B -> `' F : B -1-1-> A )
4 3 3ad2ant1 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) -> `' F : B -1-1-> A )
5 4 adantr 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> `' F : B -1-1-> A )
6 cnvimass 
 |-  ( `' `' F " C ) C_ dom `' F
7 f1of 
 |-  ( `' F : B -1-1-onto-> A -> `' F : B --> A )
8 fdm 
 |-  ( `' F : B --> A -> dom `' F = B )
9 8 eqcomd 
 |-  ( `' F : B --> A -> B = dom `' F )
10 1 7 9 3syl 
 |-  ( F : A -1-1-onto-> B -> B = dom `' F )
11 6 10 sseqtrrid 
 |-  ( F : A -1-1-onto-> B -> ( `' `' F " C ) C_ B )
12 11 3ad2ant1 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) -> ( `' `' F " C ) C_ B )
13 12 adantr 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( `' `' F " C ) C_ B )
14 f1ofn 
 |-  ( `' F : B -1-1-onto-> A -> `' F Fn B )
15 1 14 syl 
 |-  ( F : A -1-1-onto-> B -> `' F Fn B )
16 15 3ad2ant1 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) -> `' F Fn B )
17 16 adantr 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> `' F Fn B )
18 eqidd 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( ran `' F i^i C ) = ( ran `' F i^i C ) )
19 eqidd 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( `' `' F " C ) = ( `' `' F " C ) )
20 17 18 19 rescnvimafod 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( `' F |` ( `' `' F " C ) ) : ( `' `' F " C ) -onto-> ( ran `' F i^i C ) )
21 fof 
 |-  ( ( `' F |` ( `' `' F " C ) ) : ( `' `' F " C ) -onto-> ( ran `' F i^i C ) -> ( `' F |` ( `' `' F " C ) ) : ( `' `' F " C ) --> ( ran `' F i^i C ) )
22 20 21 syl 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( `' F |` ( `' `' F " C ) ) : ( `' `' F " C ) --> ( ran `' F i^i C ) )
23 f1resf1 
 |-  ( ( `' F : B -1-1-> A /\ ( `' `' F " C ) C_ B /\ ( `' F |` ( `' `' F " C ) ) : ( `' `' F " C ) --> ( ran `' F i^i C ) ) -> ( `' F |` ( `' `' F " C ) ) : ( `' `' F " C ) -1-1-> ( ran `' F i^i C ) )
24 5 13 22 23 syl3anc 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( `' F |` ( `' `' F " C ) ) : ( `' `' F " C ) -1-1-> ( ran `' F i^i C ) )
25 f1of1 
 |-  ( G : C -1-1-onto-> D -> G : C -1-1-> D )
26 25 3ad2ant2 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) -> G : C -1-1-> D )
27 26 adantr 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> G : C -1-1-> D )
28 inss2 
 |-  ( ran `' F i^i C ) C_ C
29 f1ores 
 |-  ( ( G : C -1-1-> D /\ ( ran `' F i^i C ) C_ C ) -> ( G |` ( ran `' F i^i C ) ) : ( ran `' F i^i C ) -1-1-onto-> ( G " ( ran `' F i^i C ) ) )
30 27 28 29 sylancl 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( G |` ( ran `' F i^i C ) ) : ( ran `' F i^i C ) -1-1-onto-> ( G " ( ran `' F i^i C ) ) )
31 f1ofo 
 |-  ( `' F : B -1-1-onto-> A -> `' F : B -onto-> A )
32 forn 
 |-  ( `' F : B -onto-> A -> ran `' F = A )
33 1 31 32 3syl 
 |-  ( F : A -1-1-onto-> B -> ran `' F = A )
34 33 3ad2ant1 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) -> ran `' F = A )
35 34 adantr 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ran `' F = A )
36 35 ineq1d 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( ran `' F i^i C ) = ( A i^i C ) )
37 incom 
 |-  ( A i^i C ) = ( C i^i A )
38 dfss2 
 |-  ( C C_ A <-> ( C i^i A ) = C )
39 38 biimpi 
 |-  ( C C_ A -> ( C i^i A ) = C )
40 37 39 eqtrid 
 |-  ( C C_ A -> ( A i^i C ) = C )
41 40 ad2antrl 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( A i^i C ) = C )
42 36 41 eqtrd 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( ran `' F i^i C ) = C )
43 42 imaeq2d 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( G " ( ran `' F i^i C ) ) = ( G " C ) )
44 f1ofn 
 |-  ( G : C -1-1-onto-> D -> G Fn C )
45 fnima 
 |-  ( G Fn C -> ( G " C ) = ran G )
46 44 45 syl 
 |-  ( G : C -1-1-onto-> D -> ( G " C ) = ran G )
47 f1ofo 
 |-  ( G : C -1-1-onto-> D -> G : C -onto-> D )
48 forn 
 |-  ( G : C -onto-> D -> ran G = D )
49 47 48 syl 
 |-  ( G : C -1-1-onto-> D -> ran G = D )
50 46 49 eqtrd 
 |-  ( G : C -1-1-onto-> D -> ( G " C ) = D )
51 50 3ad2ant2 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) -> ( G " C ) = D )
52 51 adantr 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( G " C ) = D )
53 43 52 eqtrd 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( G " ( ran `' F i^i C ) ) = D )
54 53 eqcomd 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> D = ( G " ( ran `' F i^i C ) ) )
55 54 f1oeq3d 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( ( G |` ( ran `' F i^i C ) ) : ( ran `' F i^i C ) -1-1-onto-> D <-> ( G |` ( ran `' F i^i C ) ) : ( ran `' F i^i C ) -1-1-onto-> ( G " ( ran `' F i^i C ) ) ) )
56 30 55 mpbird 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( G |` ( ran `' F i^i C ) ) : ( ran `' F i^i C ) -1-1-onto-> D )
57 f1orel 
 |-  ( F : A -1-1-onto-> B -> Rel F )
58 57 3ad2ant1 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) -> Rel F )
59 58 adantr 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> Rel F )
60 dfrel2 
 |-  ( Rel F <-> `' `' F = F )
61 59 60 sylib 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> `' `' F = F )
62 61 eqcomd 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> F = `' `' F )
63 62 imaeq1d 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( F " C ) = ( `' `' F " C ) )
64 63 f1oeq2d 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( ( G o. `' F ) : ( F " C ) -1-1-onto-> D <-> ( G o. `' F ) : ( `' `' F " C ) -1-1-onto-> D ) )
65 1 7 syl 
 |-  ( F : A -1-1-onto-> B -> `' F : B --> A )
66 65 3ad2ant1 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) -> `' F : B --> A )
67 66 adantr 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> `' F : B --> A )
68 eqid 
 |-  ( ran `' F i^i C ) = ( ran `' F i^i C )
69 eqid 
 |-  ( `' `' F " C ) = ( `' `' F " C )
70 eqid 
 |-  ( `' F |` ( `' `' F " C ) ) = ( `' F |` ( `' `' F " C ) )
71 f1of 
 |-  ( G : C -1-1-onto-> D -> G : C --> D )
72 71 3ad2ant2 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) -> G : C --> D )
73 72 adantr 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> G : C --> D )
74 eqid 
 |-  ( G |` ( ran `' F i^i C ) ) = ( G |` ( ran `' F i^i C ) )
75 67 68 69 70 73 74 fcoresf1ob 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( ( G o. `' F ) : ( `' `' F " C ) -1-1-onto-> D <-> ( ( `' F |` ( `' `' F " C ) ) : ( `' `' F " C ) -1-1-> ( ran `' F i^i C ) /\ ( G |` ( ran `' F i^i C ) ) : ( ran `' F i^i C ) -1-1-onto-> D ) ) )
76 64 75 bitrd 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( ( G o. `' F ) : ( F " C ) -1-1-onto-> D <-> ( ( `' F |` ( `' `' F " C ) ) : ( `' `' F " C ) -1-1-> ( ran `' F i^i C ) /\ ( G |` ( ran `' F i^i C ) ) : ( ran `' F i^i C ) -1-1-onto-> D ) ) )
77 24 56 76 mpbir2and 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( G o. `' F ) : ( F " C ) -1-1-onto-> D )
78 simpl3 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> H : E -1-1-onto-> I )
79 simprr 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> D C_ E )
80 f1ocoima 
 |-  ( ( ( G o. `' F ) : ( F " C ) -1-1-onto-> D /\ H : E -1-1-onto-> I /\ D C_ E ) -> ( H o. ( G o. `' F ) ) : ( F " C ) -1-1-onto-> ( H " D ) )
81 77 78 79 80 syl3anc 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( H o. ( G o. `' F ) ) : ( F " C ) -1-1-onto-> ( H " D ) )
82 coass 
 |-  ( ( H o. G ) o. `' F ) = ( H o. ( G o. `' F ) )
83 f1oeq1 
 |-  ( ( ( H o. G ) o. `' F ) = ( H o. ( G o. `' F ) ) -> ( ( ( H o. G ) o. `' F ) : ( F " C ) -1-1-onto-> ( H " D ) <-> ( H o. ( G o. `' F ) ) : ( F " C ) -1-1-onto-> ( H " D ) ) )
84 82 83 ax-mp 
 |-  ( ( ( H o. G ) o. `' F ) : ( F " C ) -1-1-onto-> ( H " D ) <-> ( H o. ( G o. `' F ) ) : ( F " C ) -1-1-onto-> ( H " D ) )
85 81 84 sylibr 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ H : E -1-1-onto-> I ) /\ ( C C_ A /\ D C_ E ) ) -> ( ( H o. G ) o. `' F ) : ( F " C ) -1-1-onto-> ( H " D ) )