Metamath Proof Explorer

Theorem fsovcnvlem

Description: The O operator, which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, gives a family of functions that include their own inverse. (Contributed by RP, 27-Apr-2021)

Ref Expression
Hypotheses fsovd.fs 
|- O = ( a e. _V , b e. _V |-> ( f e. ( ~P b ^m a ) |-> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) ) )
fsovd.a 
|- ( ph -> A e. V )
fsovd.b 
|- ( ph -> B e. W )
fsovfvd.g 
|- G = ( A O B )
fsovcnvlem.h 
|- H = ( B O A )
Assertion fsovcnvlem 
|- ( ph -> ( H o. G ) = ( _I |` ( ~P B ^m A ) ) )

Proof

Step Hyp Ref Expression
1 fsovd.fs 
 |-  O = ( a e. _V , b e. _V |-> ( f e. ( ~P b ^m a ) |-> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) ) )
2 fsovd.a 
 |-  ( ph -> A e. V )
3 fsovd.b 
 |-  ( ph -> B e. W )
4 fsovfvd.g 
 |-  G = ( A O B )
5 fsovcnvlem.h 
 |-  H = ( B O A )
6 ssrab2 
 |-  { x e. A | y e. ( f ` x ) } C_ A
7 6 a1i 
 |-  ( ph -> { x e. A | y e. ( f ` x ) } C_ A )
8 2 7 sselpwd 
 |-  ( ph -> { x e. A | y e. ( f ` x ) } e. ~P A )
9 8 adantr 
 |-  ( ( ph /\ y e. B ) -> { x e. A | y e. ( f ` x ) } e. ~P A )
10 9 fmpttd 
 |-  ( ph -> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) : B --> ~P A )
11 2 pwexd 
 |-  ( ph -> ~P A e. _V )
12 11 3 elmapd 
 |-  ( ph -> ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) e. ( ~P A ^m B ) <-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) : B --> ~P A ) )
13 10 12 mpbird 
 |-  ( ph -> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) e. ( ~P A ^m B ) )
14 13 adantr 
 |-  ( ( ph /\ f e. ( ~P B ^m A ) ) -> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) e. ( ~P A ^m B ) )
15 1 2 3 fsovd 
 |-  ( ph -> ( A O B ) = ( f e. ( ~P B ^m A ) |-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ) )
16 4 15 eqtrid 
 |-  ( ph -> G = ( f e. ( ~P B ^m A ) |-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ) )
17 oveq2 
 |-  ( a = d -> ( ~P b ^m a ) = ( ~P b ^m d ) )
18 rabeq 
 |-  ( a = d -> { x e. a | y e. ( f ` x ) } = { x e. d | y e. ( f ` x ) } )
19 18 mpteq2dv 
 |-  ( a = d -> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) = ( y e. b |-> { x e. d | y e. ( f ` x ) } ) )
20 17 19 mpteq12dv 
 |-  ( a = d -> ( f e. ( ~P b ^m a ) |-> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) ) = ( f e. ( ~P b ^m d ) |-> ( y e. b |-> { x e. d | y e. ( f ` x ) } ) ) )
21 pweq 
 |-  ( b = c -> ~P b = ~P c )
22 21 oveq1d 
 |-  ( b = c -> ( ~P b ^m d ) = ( ~P c ^m d ) )
23 mpteq1 
 |-  ( b = c -> ( y e. b |-> { x e. d | y e. ( f ` x ) } ) = ( y e. c |-> { x e. d | y e. ( f ` x ) } ) )
24 22 23 mpteq12dv 
 |-  ( b = c -> ( f e. ( ~P b ^m d ) |-> ( y e. b |-> { x e. d | y e. ( f ` x ) } ) ) = ( f e. ( ~P c ^m d ) |-> ( y e. c |-> { x e. d | y e. ( f ` x ) } ) ) )
25 20 24 cbvmpov 
 |-  ( a e. _V , b e. _V |-> ( f e. ( ~P b ^m a ) |-> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) ) ) = ( d e. _V , c e. _V |-> ( f e. ( ~P c ^m d ) |-> ( y e. c |-> { x e. d | y e. ( f ` x ) } ) ) )
26 eqid 
 |-  _V = _V
27 fveq1 
 |-  ( f = g -> ( f ` x ) = ( g ` x ) )
28 27 eleq2d 
 |-  ( f = g -> ( y e. ( f ` x ) <-> y e. ( g ` x ) ) )
29 28 rabbidv 
 |-  ( f = g -> { x e. d | y e. ( f ` x ) } = { x e. d | y e. ( g ` x ) } )
30 29 mpteq2dv 
 |-  ( f = g -> ( y e. c |-> { x e. d | y e. ( f ` x ) } ) = ( y e. c |-> { x e. d | y e. ( g ` x ) } ) )
31 30 cbvmptv 
 |-  ( f e. ( ~P c ^m d ) |-> ( y e. c |-> { x e. d | y e. ( f ` x ) } ) ) = ( g e. ( ~P c ^m d ) |-> ( y e. c |-> { x e. d | y e. ( g ` x ) } ) )
32 eleq1w 
 |-  ( y = u -> ( y e. ( g ` x ) <-> u e. ( g ` x ) ) )
33 32 rabbidv 
 |-  ( y = u -> { x e. d | y e. ( g ` x ) } = { x e. d | u e. ( g ` x ) } )
34 33 cbvmptv 
 |-  ( y e. c |-> { x e. d | y e. ( g ` x ) } ) = ( u e. c |-> { x e. d | u e. ( g ` x ) } )
35 fveq2 
 |-  ( x = v -> ( g ` x ) = ( g ` v ) )
36 35 eleq2d 
 |-  ( x = v -> ( u e. ( g ` x ) <-> u e. ( g ` v ) ) )
37 36 cbvrabv 
 |-  { x e. d | u e. ( g ` x ) } = { v e. d | u e. ( g ` v ) }
38 37 mpteq2i 
 |-  ( u e. c |-> { x e. d | u e. ( g ` x ) } ) = ( u e. c |-> { v e. d | u e. ( g ` v ) } )
39 34 38 eqtri 
 |-  ( y e. c |-> { x e. d | y e. ( g ` x ) } ) = ( u e. c |-> { v e. d | u e. ( g ` v ) } )
40 39 mpteq2i 
 |-  ( g e. ( ~P c ^m d ) |-> ( y e. c |-> { x e. d | y e. ( g ` x ) } ) ) = ( g e. ( ~P c ^m d ) |-> ( u e. c |-> { v e. d | u e. ( g ` v ) } ) )
41 31 40 eqtri 
 |-  ( f e. ( ~P c ^m d ) |-> ( y e. c |-> { x e. d | y e. ( f ` x ) } ) ) = ( g e. ( ~P c ^m d ) |-> ( u e. c |-> { v e. d | u e. ( g ` v ) } ) )
42 26 26 41 mpoeq123i 
 |-  ( d e. _V , c e. _V |-> ( f e. ( ~P c ^m d ) |-> ( y e. c |-> { x e. d | y e. ( f ` x ) } ) ) ) = ( d e. _V , c e. _V |-> ( g e. ( ~P c ^m d ) |-> ( u e. c |-> { v e. d | u e. ( g ` v ) } ) ) )
43 1 25 42 3eqtri 
 |-  O = ( d e. _V , c e. _V |-> ( g e. ( ~P c ^m d ) |-> ( u e. c |-> { v e. d | u e. ( g ` v ) } ) ) )
44 43 3 2 fsovd 
 |-  ( ph -> ( B O A ) = ( g e. ( ~P A ^m B ) |-> ( u e. A |-> { v e. B | u e. ( g ` v ) } ) ) )
45 5 44 eqtrid 
 |-  ( ph -> H = ( g e. ( ~P A ^m B ) |-> ( u e. A |-> { v e. B | u e. ( g ` v ) } ) ) )
46 fveq1 
 |-  ( g = ( y e. B |-> { x e. A | y e. ( f ` x ) } ) -> ( g ` v ) = ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) )
47 46 eleq2d 
 |-  ( g = ( y e. B |-> { x e. A | y e. ( f ` x ) } ) -> ( u e. ( g ` v ) <-> u e. ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) ) )
48 47 rabbidv 
 |-  ( g = ( y e. B |-> { x e. A | y e. ( f ` x ) } ) -> { v e. B | u e. ( g ` v ) } = { v e. B | u e. ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) } )
49 48 mpteq2dv 
 |-  ( g = ( y e. B |-> { x e. A | y e. ( f ` x ) } ) -> ( u e. A |-> { v e. B | u e. ( g ` v ) } ) = ( u e. A |-> { v e. B | u e. ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) } ) )
50 14 16 45 49 fmptco 
 |-  ( ph -> ( H o. G ) = ( f e. ( ~P B ^m A ) |-> ( u e. A |-> { v e. B | u e. ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) } ) ) )
51 eqidd 
 |-  ( ( ( ph /\ u e. A ) /\ v e. B ) -> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) = ( y e. B |-> { x e. A | y e. ( f ` x ) } ) )
52 eleq1w 
 |-  ( y = v -> ( y e. ( f ` x ) <-> v e. ( f ` x ) ) )
53 52 rabbidv 
 |-  ( y = v -> { x e. A | y e. ( f ` x ) } = { x e. A | v e. ( f ` x ) } )
54 53 adantl 
 |-  ( ( ( ( ph /\ u e. A ) /\ v e. B ) /\ y = v ) -> { x e. A | y e. ( f ` x ) } = { x e. A | v e. ( f ` x ) } )
55 simpr 
 |-  ( ( ( ph /\ u e. A ) /\ v e. B ) -> v e. B )
56 rabexg 
 |-  ( A e. V -> { x e. A | v e. ( f ` x ) } e. _V )
57 2 56 syl 
 |-  ( ph -> { x e. A | v e. ( f ` x ) } e. _V )
58 57 ad2antrr 
 |-  ( ( ( ph /\ u e. A ) /\ v e. B ) -> { x e. A | v e. ( f ` x ) } e. _V )
59 51 54 55 58 fvmptd 
 |-  ( ( ( ph /\ u e. A ) /\ v e. B ) -> ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) = { x e. A | v e. ( f ` x ) } )
60 59 eleq2d 
 |-  ( ( ( ph /\ u e. A ) /\ v e. B ) -> ( u e. ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) <-> u e. { x e. A | v e. ( f ` x ) } ) )
61 fveq2 
 |-  ( x = u -> ( f ` x ) = ( f ` u ) )
62 61 eleq2d 
 |-  ( x = u -> ( v e. ( f ` x ) <-> v e. ( f ` u ) ) )
63 62 elrab3 
 |-  ( u e. A -> ( u e. { x e. A | v e. ( f ` x ) } <-> v e. ( f ` u ) ) )
64 63 ad2antlr 
 |-  ( ( ( ph /\ u e. A ) /\ v e. B ) -> ( u e. { x e. A | v e. ( f ` x ) } <-> v e. ( f ` u ) ) )
65 60 64 bitrd 
 |-  ( ( ( ph /\ u e. A ) /\ v e. B ) -> ( u e. ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) <-> v e. ( f ` u ) ) )
66 65 rabbidva 
 |-  ( ( ph /\ u e. A ) -> { v e. B | u e. ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) } = { v e. B | v e. ( f ` u ) } )
67 66 adantlr 
 |-  ( ( ( ph /\ f e. ( ~P B ^m A ) ) /\ u e. A ) -> { v e. B | u e. ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) } = { v e. B | v e. ( f ` u ) } )
68 elmapi 
 |-  ( f e. ( ~P B ^m A ) -> f : A --> ~P B )
69 68 ad2antlr 
 |-  ( ( ( ph /\ f e. ( ~P B ^m A ) ) /\ u e. A ) -> f : A --> ~P B )
70 simpr 
 |-  ( ( ( ph /\ f e. ( ~P B ^m A ) ) /\ u e. A ) -> u e. A )
71 69 70 ffvelrnd 
 |-  ( ( ( ph /\ f e. ( ~P B ^m A ) ) /\ u e. A ) -> ( f ` u ) e. ~P B )
72 71 elpwid 
 |-  ( ( ( ph /\ f e. ( ~P B ^m A ) ) /\ u e. A ) -> ( f ` u ) C_ B )
73 sseqin2 
 |-  ( ( f ` u ) C_ B <-> ( B i^i ( f ` u ) ) = ( f ` u ) )
74 72 73 sylib 
 |-  ( ( ( ph /\ f e. ( ~P B ^m A ) ) /\ u e. A ) -> ( B i^i ( f ` u ) ) = ( f ` u ) )
75 dfin5 
 |-  ( B i^i ( f ` u ) ) = { v e. B | v e. ( f ` u ) }
76 74 75 eqtr3di 
 |-  ( ( ( ph /\ f e. ( ~P B ^m A ) ) /\ u e. A ) -> ( f ` u ) = { v e. B | v e. ( f ` u ) } )
77 67 76 eqtr4d 
 |-  ( ( ( ph /\ f e. ( ~P B ^m A ) ) /\ u e. A ) -> { v e. B | u e. ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) } = ( f ` u ) )
78 77 mpteq2dva 
 |-  ( ( ph /\ f e. ( ~P B ^m A ) ) -> ( u e. A |-> { v e. B | u e. ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) } ) = ( u e. A |-> ( f ` u ) ) )
79 68 feqmptd 
 |-  ( f e. ( ~P B ^m A ) -> f = ( u e. A |-> ( f ` u ) ) )
80 79 adantl 
 |-  ( ( ph /\ f e. ( ~P B ^m A ) ) -> f = ( u e. A |-> ( f ` u ) ) )
81 78 80 eqtr4d 
 |-  ( ( ph /\ f e. ( ~P B ^m A ) ) -> ( u e. A |-> { v e. B | u e. ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) } ) = f )
82 81 mpteq2dva 
 |-  ( ph -> ( f e. ( ~P B ^m A ) |-> ( u e. A |-> { v e. B | u e. ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ` v ) } ) ) = ( f e. ( ~P B ^m A ) |-> f ) )
83 mptresid 
 |-  ( _I |` ( ~P B ^m A ) ) = ( f e. ( ~P B ^m A ) |-> f )
84 83 eqcomi 
 |-  ( f e. ( ~P B ^m A ) |-> f ) = ( _I |` ( ~P B ^m A ) )
85 84 a1i 
 |-  ( ph -> ( f e. ( ~P B ^m A ) |-> f ) = ( _I |` ( ~P B ^m A ) ) )
86 50 82 85 3eqtrd 
 |-  ( ph -> ( H o. G ) = ( _I |` ( ~P B ^m A ) ) )