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 \in 𝒫 Y ⟼ F^{-1} [n])$
	pwrssmgc.2	$⊢ H = (m \in 𝒫 X ⟼ \{y \in Y \| F^{-1} [\{y\}] \subseteq m\})$
	pwrssmgc.3	$⊢ V = toInc (𝒫 Y)$
	pwrssmgc.4	$⊢ W = toInc (𝒫 X)$
	pwrssmgc.5	$⊢ φ \to X \in A$
	pwrssmgc.6	$⊢ φ \to Y \in B$
	pwrssmgc.7	$⊢ φ \to F : X ⟶ Y$
Assertion	pwrssmgc	$⊢ φ \to G (V MGalConn W) H$

Proof

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

Metamath Proof Explorer

Theorem pwrssmgc

Proof