Metamath Proof Explorer

Theorem pwrssmgc

Description: Given a function F , exhibit a Galois connection between subsets of its domain and subsets of its range. (Contributed by Thierry Arnoux, 26-Apr-2024)

Ref Expression
Hypotheses pwrssmgc.1 
|- G = ( n e. ~P Y |-> ( `' F " n ) )
pwrssmgc.2 
|- H = ( m e. ~P X |-> { y e. Y | ( `' F " { y } ) C_ m } )
pwrssmgc.3 
|- V = ( toInc ` ~P Y )
pwrssmgc.4 
|- W = ( toInc ` ~P X )
pwrssmgc.5 
|- ( ph -> X e. A )
pwrssmgc.6 
|- ( ph -> Y e. B )
pwrssmgc.7 
|- ( ph -> F : X --> Y )
Assertion pwrssmgc 
|- ( ph -> G ( V MGalConn W ) H )

Proof

Step Hyp Ref Expression
1 pwrssmgc.1 
 |-  G = ( n e. ~P Y |-> ( `' F " n ) )
2 pwrssmgc.2 
 |-  H = ( m e. ~P X |-> { y e. Y | ( `' F " { y } ) C_ m } )
3 pwrssmgc.3 
 |-  V = ( toInc ` ~P Y )
4 pwrssmgc.4 
 |-  W = ( toInc ` ~P X )
5 pwrssmgc.5 
 |-  ( ph -> X e. A )
6 pwrssmgc.6 
 |-  ( ph -> Y e. B )
7 pwrssmgc.7 
 |-  ( ph -> F : X --> Y )
8 5 adantr 
 |-  ( ( ph /\ n e. ~P Y ) -> X e. A )
9 cnvimass 
 |-  ( `' F " n ) C_ dom F
10 9 7 fssdm 
 |-  ( ph -> ( `' F " n ) C_ X )
11 10 adantr 
 |-  ( ( ph /\ n e. ~P Y ) -> ( `' F " n ) C_ X )
12 8 11 sselpwd 
 |-  ( ( ph /\ n e. ~P Y ) -> ( `' F " n ) e. ~P X )
13 12 1 fmptd 
 |-  ( ph -> G : ~P Y --> ~P X )
14 pwexg 
 |-  ( Y e. B -> ~P Y e. _V )
15 3 ipobas 
 |-  ( ~P Y e. _V -> ~P Y = ( Base ` V ) )
16 6 14 15 3syl 
 |-  ( ph -> ~P Y = ( Base ` V ) )
17 pwexg 
 |-  ( X e. A -> ~P X e. _V )
18 4 ipobas 
 |-  ( ~P X e. _V -> ~P X = ( Base ` W ) )
19 5 17 18 3syl 
 |-  ( ph -> ~P X = ( Base ` W ) )
20 16 19 feq23d 
 |-  ( ph -> ( G : ~P Y --> ~P X <-> G : ( Base ` V ) --> ( Base ` W ) ) )
21 13 20 mpbid 
 |-  ( ph -> G : ( Base ` V ) --> ( Base ` W ) )
22 6 adantr 
 |-  ( ( ph /\ m e. ~P X ) -> Y e. B )
23 ssrab2 
 |-  { y e. Y | ( `' F " { y } ) C_ m } C_ Y
24 23 a1i 
 |-  ( ( ph /\ m e. ~P X ) -> { y e. Y | ( `' F " { y } ) C_ m } C_ Y )
25 22 24 sselpwd 
 |-  ( ( ph /\ m e. ~P X ) -> { y e. Y | ( `' F " { y } ) C_ m } e. ~P Y )
26 25 2 fmptd 
 |-  ( ph -> H : ~P X --> ~P Y )
27 19 16 feq23d 
 |-  ( ph -> ( H : ~P X --> ~P Y <-> H : ( Base ` W ) --> ( Base ` V ) ) )
28 26 27 mpbid 
 |-  ( ph -> H : ( Base ` W ) --> ( Base ` V ) )
29 21 28 jca 
 |-  ( ph -> ( G : ( Base ` V ) --> ( Base ` W ) /\ H : ( Base ` W ) --> ( Base ` V ) ) )
30 sneq 
 |-  ( y = j -> { y } = { j } )
31 30 imaeq2d 
 |-  ( y = j -> ( `' F " { y } ) = ( `' F " { j } ) )
32 31 sseq1d 
 |-  ( y = j -> ( ( `' F " { y } ) C_ v <-> ( `' F " { j } ) C_ v ) )
33 simplr 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> u e. ( Base ` V ) )
34 16 ad2antrr 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ~P Y = ( Base ` V ) )
35 33 34 eleqtrrd 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> u e. ~P Y )
36 35 adantr 
 |-  ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ ( `' F " u ) C_ v ) -> u e. ~P Y )
37 36 elpwid 
 |-  ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ ( `' F " u ) C_ v ) -> u C_ Y )
38 37 sselda 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ ( `' F " u ) C_ v ) /\ j e. u ) -> j e. Y )
39 7 ffund 
 |-  ( ph -> Fun F )
40 39 ad4antr 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ ( `' F " u ) C_ v ) /\ j e. u ) -> Fun F )
41 snssi 
 |-  ( j e. u -> { j } C_ u )
42 41 adantl 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ ( `' F " u ) C_ v ) /\ j e. u ) -> { j } C_ u )
43 sspreima 
 |-  ( ( Fun F /\ { j } C_ u ) -> ( `' F " { j } ) C_ ( `' F " u ) )
44 40 42 43 syl2anc 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ ( `' F " u ) C_ v ) /\ j e. u ) -> ( `' F " { j } ) C_ ( `' F " u ) )
45 simplr 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ ( `' F " u ) C_ v ) /\ j e. u ) -> ( `' F " u ) C_ v )
46 44 45 sstrd 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ ( `' F " u ) C_ v ) /\ j e. u ) -> ( `' F " { j } ) C_ v )
47 32 38 46 elrabd 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ ( `' F " u ) C_ v ) /\ j e. u ) -> j e. { y e. Y | ( `' F " { y } ) C_ v } )
48 47 ex 
 |-  ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ ( `' F " u ) C_ v ) -> ( j e. u -> j e. { y e. Y | ( `' F " { y } ) C_ v } ) )
49 48 ssrdv 
 |-  ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ ( `' F " u ) C_ v ) -> u C_ { y e. Y | ( `' F " { y } ) C_ v } )
50 simplr 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ u C_ { y e. Y | ( `' F " { y } ) C_ v } ) /\ i e. ( `' F " u ) ) -> u C_ { y e. Y | ( `' F " { y } ) C_ v } )
51 7 ffnd 
 |-  ( ph -> F Fn X )
52 51 ad4antr 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ u C_ { y e. Y | ( `' F " { y } ) C_ v } ) /\ i e. ( `' F " u ) ) -> F Fn X )
53 simpr 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ u C_ { y e. Y | ( `' F " { y } ) C_ v } ) /\ i e. ( `' F " u ) ) -> i e. ( `' F " u ) )
54 elpreima 
 |-  ( F Fn X -> ( i e. ( `' F " u ) <-> ( i e. X /\ ( F ` i ) e. u ) ) )
55 54 biimpa 
 |-  ( ( F Fn X /\ i e. ( `' F " u ) ) -> ( i e. X /\ ( F ` i ) e. u ) )
56 52 53 55 syl2anc 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ u C_ { y e. Y | ( `' F " { y } ) C_ v } ) /\ i e. ( `' F " u ) ) -> ( i e. X /\ ( F ` i ) e. u ) )
57 56 simprd 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ u C_ { y e. Y | ( `' F " { y } ) C_ v } ) /\ i e. ( `' F " u ) ) -> ( F ` i ) e. u )
58 50 57 sseldd 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ u C_ { y e. Y | ( `' F " { y } ) C_ v } ) /\ i e. ( `' F " u ) ) -> ( F ` i ) e. { y e. Y | ( `' F " { y } ) C_ v } )
59 sneq 
 |-  ( y = ( F ` i ) -> { y } = { ( F ` i ) } )
60 59 imaeq2d 
 |-  ( y = ( F ` i ) -> ( `' F " { y } ) = ( `' F " { ( F ` i ) } ) )
61 60 sseq1d 
 |-  ( y = ( F ` i ) -> ( ( `' F " { y } ) C_ v <-> ( `' F " { ( F ` i ) } ) C_ v ) )
62 61 elrab 
 |-  ( ( F ` i ) e. { y e. Y | ( `' F " { y } ) C_ v } <-> ( ( F ` i ) e. Y /\ ( `' F " { ( F ` i ) } ) C_ v ) )
63 62 simprbi 
 |-  ( ( F ` i ) e. { y e. Y | ( `' F " { y } ) C_ v } -> ( `' F " { ( F ` i ) } ) C_ v )
64 58 63 syl 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ u C_ { y e. Y | ( `' F " { y } ) C_ v } ) /\ i e. ( `' F " u ) ) -> ( `' F " { ( F ` i ) } ) C_ v )
65 56 simpld 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ u C_ { y e. Y | ( `' F " { y } ) C_ v } ) /\ i e. ( `' F " u ) ) -> i e. X )
66 eqidd 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ u C_ { y e. Y | ( `' F " { y } ) C_ v } ) /\ i e. ( `' F " u ) ) -> ( F ` i ) = ( F ` i ) )
67 fniniseg 
 |-  ( F Fn X -> ( i e. ( `' F " { ( F ` i ) } ) <-> ( i e. X /\ ( F ` i ) = ( F ` i ) ) ) )
68 67 biimpar 
 |-  ( ( F Fn X /\ ( i e. X /\ ( F ` i ) = ( F ` i ) ) ) -> i e. ( `' F " { ( F ` i ) } ) )
69 52 65 66 68 syl12anc 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ u C_ { y e. Y | ( `' F " { y } ) C_ v } ) /\ i e. ( `' F " u ) ) -> i e. ( `' F " { ( F ` i ) } ) )
70 64 69 sseldd 
 |-  ( ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ u C_ { y e. Y | ( `' F " { y } ) C_ v } ) /\ i e. ( `' F " u ) ) -> i e. v )
71 70 ex 
 |-  ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ u C_ { y e. Y | ( `' F " { y } ) C_ v } ) -> ( i e. ( `' F " u ) -> i e. v ) )
72 71 ssrdv 
 |-  ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ u C_ { y e. Y | ( `' F " { y } ) C_ v } ) -> ( `' F " u ) C_ v )
73 49 72 impbida 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ( ( `' F " u ) C_ v <-> u C_ { y e. Y | ( `' F " { y } ) C_ v } ) )
74 simpr 
 |-  ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ n = u ) -> n = u )
75 74 imaeq2d 
 |-  ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ n = u ) -> ( `' F " n ) = ( `' F " u ) )
76 7 5 fexd 
 |-  ( ph -> F e. _V )
77 cnvexg 
 |-  ( F e. _V -> `' F e. _V )
78 imaexg 
 |-  ( `' F e. _V -> ( `' F " u ) e. _V )
79 76 77 78 3syl 
 |-  ( ph -> ( `' F " u ) e. _V )
80 79 ad2antrr 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ( `' F " u ) e. _V )
81 1 75 35 80 fvmptd2 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ( G ` u ) = ( `' F " u ) )
82 81 sseq1d 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ( ( G ` u ) C_ v <-> ( `' F " u ) C_ v ) )
83 simpr 
 |-  ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ m = v ) -> m = v )
84 83 sseq2d 
 |-  ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ m = v ) -> ( ( `' F " { y } ) C_ m <-> ( `' F " { y } ) C_ v ) )
85 84 rabbidv 
 |-  ( ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) /\ m = v ) -> { y e. Y | ( `' F " { y } ) C_ m } = { y e. Y | ( `' F " { y } ) C_ v } )
86 simpr 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> v e. ( Base ` W ) )
87 5 17 syl 
 |-  ( ph -> ~P X e. _V )
88 87 ad2antrr 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ~P X e. _V )
89 88 18 syl 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ~P X = ( Base ` W ) )
90 86 89 eleqtrrd 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> v e. ~P X )
91 6 ad2antrr 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> Y e. B )
92 ssrab2 
 |-  { y e. Y | ( `' F " { y } ) C_ v } C_ Y
93 92 a1i 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> { y e. Y | ( `' F " { y } ) C_ v } C_ Y )
94 91 93 sselpwd 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> { y e. Y | ( `' F " { y } ) C_ v } e. ~P Y )
95 2 85 90 94 fvmptd2 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ( H ` v ) = { y e. Y | ( `' F " { y } ) C_ v } )
96 95 sseq2d 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ( u C_ ( H ` v ) <-> u C_ { y e. Y | ( `' F " { y } ) C_ v } ) )
97 73 82 96 3bitr4d 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ( ( G ` u ) C_ v <-> u C_ ( H ` v ) ) )
98 13 ad2antrr 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> G : ~P Y --> ~P X )
99 98 35 ffvelcdmd 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ( G ` u ) e. ~P X )
100 eqid 
 |-  ( le ` W ) = ( le ` W )
101 4 100 ipole 
 |-  ( ( ~P X e. _V /\ ( G ` u ) e. ~P X /\ v e. ~P X ) -> ( ( G ` u ) ( le ` W ) v <-> ( G ` u ) C_ v ) )
102 88 99 90 101 syl3anc 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ( ( G ` u ) ( le ` W ) v <-> ( G ` u ) C_ v ) )
103 6 14 syl 
 |-  ( ph -> ~P Y e. _V )
104 103 ad2antrr 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ~P Y e. _V )
105 26 ad2antrr 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> H : ~P X --> ~P Y )
106 105 90 ffvelcdmd 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ( H ` v ) e. ~P Y )
107 eqid 
 |-  ( le ` V ) = ( le ` V )
108 3 107 ipole 
 |-  ( ( ~P Y e. _V /\ u e. ~P Y /\ ( H ` v ) e. ~P Y ) -> ( u ( le ` V ) ( H ` v ) <-> u C_ ( H ` v ) ) )
109 104 35 106 108 syl3anc 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ( u ( le ` V ) ( H ` v ) <-> u C_ ( H ` v ) ) )
110 97 102 109 3bitr4d 
 |-  ( ( ( ph /\ u e. ( Base ` V ) ) /\ v e. ( Base ` W ) ) -> ( ( G ` u ) ( le ` W ) v <-> u ( le ` V ) ( H ` v ) ) )
111 110 anasss 
 |-  ( ( ph /\ ( u e. ( Base ` V ) /\ v e. ( Base ` W ) ) ) -> ( ( G ` u ) ( le ` W ) v <-> u ( le ` V ) ( H ` v ) ) )
112 111 ralrimivva 
 |-  ( ph -> A. u e. ( Base ` V ) A. v e. ( Base ` W ) ( ( G ` u ) ( le ` W ) v <-> u ( le ` V ) ( H ` v ) ) )
113 eqid 
 |-  ( Base ` V ) = ( Base ` V )
114 eqid 
 |-  ( Base ` W ) = ( Base ` W )
115 eqid 
 |-  ( V MGalConn W ) = ( V MGalConn W )
116 3 ipopos 
 |-  V e. Poset
117 posprs 
 |-  ( V e. Poset -> V e. Proset )
118 116 117 mp1i 
 |-  ( ph -> V e. Proset )
119 4 ipopos 
 |-  W e. Poset
120 posprs 
 |-  ( W e. Poset -> W e. Proset )
121 119 120 mp1i 
 |-  ( ph -> W e. Proset )
122 113 114 107 100 115 118 121 mgcval 
 |-  ( ph -> ( G ( V MGalConn W ) H <-> ( ( G : ( Base ` V ) --> ( Base ` W ) /\ H : ( Base ` W ) --> ( Base ` V ) ) /\ A. u e. ( Base ` V ) A. v e. ( Base ` W ) ( ( G ` u ) ( le ` W ) v <-> u ( le ` V ) ( H ` v ) ) ) ) )
123 29 112 122 mpbir2and 
 |-  ( ph -> G ( V MGalConn W ) H )