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	Could not format assertion : No typesetting found for \|- ( ph -> G ( V MGalConn W ) H ) with typecode \|-

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		fex	$⊢ (F : X ⟶ Y \land X \in A) \to F \in V$
77	7 5 76	syl2anc	$⊢ φ \to F \in V$
78		cnvexg	$⊢ F \in V \to F^{-1} \in V$
79		imaexg	$⊢ F^{-1} \in V \to F^{-1} [u] \in V$
80	77 78 79	3syl	$⊢ φ \to F^{-1} [u] \in V$
81	80	ad2antrr	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to F^{-1} [u] \in V$
82	1 75 35 81	fvmptd2	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to G (u) = F^{-1} [u]$
83	82	sseq1d	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to (G (u) \subseteq v \leftrightarrow F^{-1} [u] \subseteq v)$
84		simpr	$⊢ (((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \land m = v) \to m = v$
85	84	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)$
86	85	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\}$
87		simpr	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to v \in {Base}_{W}$
88	5 17	syl	$⊢ φ \to 𝒫 X \in V$
89	88	ad2antrr	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to 𝒫 X \in V$
90	89 18	syl	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to 𝒫 X = {Base}_{W}$
91	87 90	eleqtrrd	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to v \in 𝒫 X$
92	6	ad2antrr	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to Y \in B$
93		ssrab2	$⊢ \{y \in Y \| F^{-1} [\{y\}] \subseteq v\} \subseteq Y$
94	93	a1i	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to \{y \in Y \| F^{-1} [\{y\}] \subseteq v\} \subseteq Y$
95	92 94	sselpwd	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to \{y \in Y \| F^{-1} [\{y\}] \subseteq v\} \in 𝒫 Y$
96	2 86 91 95	fvmptd2	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to H (v) = \{y \in Y \| F^{-1} [\{y\}] \subseteq v\}$
97	96	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\})$
98	73 83 97	3bitr4d	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to (G (u) \subseteq v \leftrightarrow u \subseteq H (v))$
99	13	ad2antrr	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to G : 𝒫 Y ⟶ 𝒫 X$
100	99 35	ffvelrnd	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to G (u) \in 𝒫 X$
101		eqid	$⊢ \leq_{W} = \leq_{W}$
102	4 101	ipole	$⊢ (𝒫 X \in V \land G (u) \in 𝒫 X \land v \in 𝒫 X) \to (G (u) \leq_{W} v \leftrightarrow G (u) \subseteq v)$
103	89 100 91 102	syl3anc	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to (G (u) \leq_{W} v \leftrightarrow G (u) \subseteq v)$
104	6 14	syl	$⊢ φ \to 𝒫 Y \in V$
105	104	ad2antrr	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to 𝒫 Y \in V$
106	26	ad2antrr	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to H : 𝒫 X ⟶ 𝒫 Y$
107	106 91	ffvelrnd	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to H (v) \in 𝒫 Y$
108		eqid	$⊢ \leq_{V} = \leq_{V}$
109	3 108	ipole	$⊢ (𝒫 Y \in V \land u \in 𝒫 Y \land H (v) \in 𝒫 Y) \to (u \leq_{V} H (v) \leftrightarrow u \subseteq H (v))$
110	105 35 107 109	syl3anc	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to (u \leq_{V} H (v) \leftrightarrow u \subseteq H (v))$
111	98 103 110	3bitr4d	$⊢ ((φ \land u \in {Base}_{V}) \land v \in {Base}_{W}) \to (G (u) \leq_{W} v \leftrightarrow u \leq_{V} H (v))$
112	111	anasss	$⊢ (φ \land (u \in {Base}_{V} \land v \in {Base}_{W})) \to (G (u) \leq_{W} v \leftrightarrow u \leq_{V} H (v))$
113	112	ralrimivva	$⊢ φ \to \forall u \in {Base}_{V} \forall v \in {Base}_{W} (G (u) \leq_{W} v \leftrightarrow u \leq_{V} H (v))$
114		eqid	$⊢ {Base}_{V} = {Base}_{V}$
115		eqid	$⊢ {Base}_{W} = {Base}_{W}$
116		eqid	Could not format ( V MGalConn W ) = ( V MGalConn W ) : No typesetting found for \|- ( V MGalConn W ) = ( V MGalConn W ) with typecode \|-
117	3	ipopos	$⊢ V \in Poset$
118		posprs	$⊢ V \in Poset \to V \in Proset$
119	117 118	mp1i	$⊢ φ \to V \in Proset$
120	4	ipopos	$⊢ W \in Poset$
121		posprs	$⊢ W \in Poset \to W \in Proset$
122	120 121	mp1i	$⊢ φ \to W \in Proset$
123	114 115 108 101 116 119 122	mgcval	Could not format ( 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 ) ) ) ) ) : No typesetting found for \|- ( 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 ) ) ) ) ) with typecode \|-
124	29 113 123	mpbir2and	Could not format ( ph -> G ( V MGalConn W ) H ) : No typesetting found for \|- ( ph -> G ( V MGalConn W ) H ) with typecode \|-

Metamath Proof Explorer

Theorem pwrssmgc

Proof