Metamath Proof Explorer

Theorem f1ossf1o

Description: Restricting a bijection, which is a mapping from a restricted class abstraction, to a subset is a bijection. (Contributed by AV, 7-Aug-2022)

Ref Expression
Hypotheses f1ossf1o.x 
|- X = { w e. A | ( ps /\ ch ) }
f1ossf1o.y 
|- Y = { w e. A | ps }
f1ossf1o.f 
|- F = ( x e. X |-> B )
f1ossf1o.g 
|- G = ( x e. Y |-> B )
f1ossf1o.b 
|- ( ph -> G : Y -1-1-onto-> C )
f1ossf1o.s 
|- ( ( ph /\ x e. Y /\ y = B ) -> ( ta <-> [ x / w ] ch ) )
Assertion f1ossf1o 
|- ( ph -> F : X -1-1-onto-> { y e. C | ta } )

Proof

Step Hyp Ref Expression
1 f1ossf1o.x 
 |-  X = { w e. A | ( ps /\ ch ) }
2 f1ossf1o.y 
 |-  Y = { w e. A | ps }
3 f1ossf1o.f 
 |-  F = ( x e. X |-> B )
4 f1ossf1o.g 
 |-  G = ( x e. Y |-> B )
5 f1ossf1o.b 
 |-  ( ph -> G : Y -1-1-onto-> C )
6 f1ossf1o.s 
 |-  ( ( ph /\ x e. Y /\ y = B ) -> ( ta <-> [ x / w ] ch ) )
7 4 5 6 f1oresrab 
 |-  ( ph -> ( G |` { x e. Y | [ x / w ] ch } ) : { x e. Y | [ x / w ] ch } -1-1-onto-> { y e. C | ta } )
8 simpl 
 |-  ( ( ps /\ ch ) -> ps )
9 8 a1i 
 |-  ( w e. A -> ( ( ps /\ ch ) -> ps ) )
10 9 ss2rabi 
 |-  { w e. A | ( ps /\ ch ) } C_ { w e. A | ps }
11 10 1 2 3sstr4i 
 |-  X C_ Y
12 11 a1i 
 |-  ( ph -> X C_ Y )
13 12 resmptd 
 |-  ( ph -> ( ( x e. Y |-> B ) |` X ) = ( x e. X |-> B ) )
14 4 a1i 
 |-  ( ph -> G = ( x e. Y |-> B ) )
15 2 rabeqi 
 |-  { x e. Y | [ x / w ] ch } = { x e. { w e. A | ps } | [ x / w ] ch }
16 nfcv 
 |-  F/_ w x
17 nfcv 
 |-  F/_ w A
18 nfs1v 
 |-  F/ w [ x / w ] ps
19 sbequ12 
 |-  ( w = x -> ( ps <-> [ x / w ] ps ) )
20 16 17 18 19 elrabf 
 |-  ( x e. { w e. A | ps } <-> ( x e. A /\ [ x / w ] ps ) )
21 20 anbi1i 
 |-  ( ( x e. { w e. A | ps } /\ [ x / w ] ch ) <-> ( ( x e. A /\ [ x / w ] ps ) /\ [ x / w ] ch ) )
22 anass 
 |-  ( ( ( x e. A /\ [ x / w ] ps ) /\ [ x / w ] ch ) <-> ( x e. A /\ ( [ x / w ] ps /\ [ x / w ] ch ) ) )
23 21 22 bitri 
 |-  ( ( x e. { w e. A | ps } /\ [ x / w ] ch ) <-> ( x e. A /\ ( [ x / w ] ps /\ [ x / w ] ch ) ) )
24 23 rabbia2 
 |-  { x e. { w e. A | ps } | [ x / w ] ch } = { x e. A | ( [ x / w ] ps /\ [ x / w ] ch ) }
25 nfcv 
 |-  F/_ x A
26 nfv 
 |-  F/ x ( ps /\ ch )
27 nfs1v 
 |-  F/ w [ x / w ] ch
28 18 27 nfan 
 |-  F/ w ( [ x / w ] ps /\ [ x / w ] ch )
29 sbequ12 
 |-  ( w = x -> ( ch <-> [ x / w ] ch ) )
30 19 29 anbi12d 
 |-  ( w = x -> ( ( ps /\ ch ) <-> ( [ x / w ] ps /\ [ x / w ] ch ) ) )
31 17 25 26 28 30 cbvrabw 
 |-  { w e. A | ( ps /\ ch ) } = { x e. A | ( [ x / w ] ps /\ [ x / w ] ch ) }
32 1 31 eqtr2i 
 |-  { x e. A | ( [ x / w ] ps /\ [ x / w ] ch ) } = X
33 15 24 32 3eqtri 
 |-  { x e. Y | [ x / w ] ch } = X
34 33 a1i 
 |-  ( ph -> { x e. Y | [ x / w ] ch } = X )
35 14 34 reseq12d 
 |-  ( ph -> ( G |` { x e. Y | [ x / w ] ch } ) = ( ( x e. Y |-> B ) |` X ) )
36 3 a1i 
 |-  ( ph -> F = ( x e. X |-> B ) )
37 13 35 36 3eqtr4rd 
 |-  ( ph -> F = ( G |` { x e. Y | [ x / w ] ch } ) )
38 15 24 eqtr2i 
 |-  { x e. A | ( [ x / w ] ps /\ [ x / w ] ch ) } = { x e. Y | [ x / w ] ch }
39 1 31 38 3eqtri 
 |-  X = { x e. Y | [ x / w ] ch }
40 39 a1i 
 |-  ( ph -> X = { x e. Y | [ x / w ] ch } )
41 eqidd 
 |-  ( ph -> { y e. C | ta } = { y e. C | ta } )
42 37 40 41 f1oeq123d 
 |-  ( ph -> ( F : X -1-1-onto-> { y e. C | ta } <-> ( G |` { x e. Y | [ x / w ] ch } ) : { x e. Y | [ x / w ] ch } -1-1-onto-> { y e. C | ta } ) )
43 7 42 mpbird 
 |-  ( ph -> F : X -1-1-onto-> { y e. C | ta } )