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 ⊢ 𝐺 = ( 𝑛 ∈ 𝒫 𝑌 ↦ ( ◡ 𝐹 “ 𝑛 ) )
pwrssmgc.2 ⊢ 𝐻 = ( 𝑚 ∈ 𝒫 𝑋 ↦ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑚 } )
pwrssmgc.3 ⊢ 𝑉 = ( toInc ‘ 𝒫 𝑌 )
pwrssmgc.4 ⊢ 𝑊 = ( toInc ‘ 𝒫 𝑋 )
pwrssmgc.5 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
pwrssmgc.6 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
pwrssmgc.7 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
Assertion pwrssmgc ( 𝜑 → 𝐺 ( 𝑉 MGalConn 𝑊 ) 𝐻 )

Proof

Step Hyp Ref Expression
1 pwrssmgc.1 ⊢ 𝐺 = ( 𝑛 ∈ 𝒫 𝑌 ↦ ( ◡ 𝐹 “ 𝑛 ) )
2 pwrssmgc.2 ⊢ 𝐻 = ( 𝑚 ∈ 𝒫 𝑋 ↦ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑚 } )
3 pwrssmgc.3 ⊢ 𝑉 = ( toInc ‘ 𝒫 𝑌 )
4 pwrssmgc.4 ⊢ 𝑊 = ( toInc ‘ 𝒫 𝑋 )
5 pwrssmgc.5 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
6 pwrssmgc.6 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 pwrssmgc.7 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
8 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝒫 𝑌 ) → 𝑋 ∈ 𝐴 )
9 cnvimass ⊢ ( ◡ 𝐹 “ 𝑛 ) ⊆ dom 𝐹
10 9 7 fssdm ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑛 ) ⊆ 𝑋 )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝒫 𝑌 ) → ( ◡ 𝐹 “ 𝑛 ) ⊆ 𝑋 )
12 8 11 sselpwd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝒫 𝑌 ) → ( ◡ 𝐹 “ 𝑛 ) ∈ 𝒫 𝑋 )
13 12 1 fmptd ⊢ ( 𝜑 → 𝐺 : 𝒫 𝑌 ⟶ 𝒫 𝑋 )
14 pwexg ⊢ ( 𝑌 ∈ 𝐵 → 𝒫 𝑌 ∈ V )
15 3 ipobas ⊢ ( 𝒫 𝑌 ∈ V → 𝒫 𝑌 = ( Base ‘ 𝑉 ) )
16 6 14 15 3syl ⊢ ( 𝜑 → 𝒫 𝑌 = ( Base ‘ 𝑉 ) )
17 pwexg ⊢ ( 𝑋 ∈ 𝐴 → 𝒫 𝑋 ∈ V )
18 4 ipobas ⊢ ( 𝒫 𝑋 ∈ V → 𝒫 𝑋 = ( Base ‘ 𝑊 ) )
19 5 17 18 3syl ⊢ ( 𝜑 → 𝒫 𝑋 = ( Base ‘ 𝑊 ) )
20 16 19 feq23d ⊢ ( 𝜑 → ( 𝐺 : 𝒫 𝑌 ⟶ 𝒫 𝑋 ↔ 𝐺 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ) )
21 13 20 mpbid ⊢ ( 𝜑 → 𝐺 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) )
22 6 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝒫 𝑋 ) → 𝑌 ∈ 𝐵 )
23 ssrab2 ⊢ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑚 } ⊆ 𝑌
24 23 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝒫 𝑋 ) → { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑚 } ⊆ 𝑌 )
25 22 24 sselpwd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝒫 𝑋 ) → { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑚 } ∈ 𝒫 𝑌 )
26 25 2 fmptd ⊢ ( 𝜑 → 𝐻 : 𝒫 𝑋 ⟶ 𝒫 𝑌 )
27 19 16 feq23d ⊢ ( 𝜑 → ( 𝐻 : 𝒫 𝑋 ⟶ 𝒫 𝑌 ↔ 𝐻 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ) )
28 26 27 mpbid ⊢ ( 𝜑 → 𝐻 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) )
29 21 28 jca ⊢ ( 𝜑 → ( 𝐺 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ∧ 𝐻 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ) )
30 sneq ⊢ ( 𝑦 = 𝑗 → { 𝑦 } = { 𝑗 } )
31 30 imaeq2d ⊢ ( 𝑦 = 𝑗 → ( ◡ 𝐹 “ { 𝑦 } ) = ( ◡ 𝐹 “ { 𝑗 } ) )
32 31 sseq1d ⊢ ( 𝑦 = 𝑗 → ( ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 ↔ ( ◡ 𝐹 “ { 𝑗 } ) ⊆ 𝑣 ) )
33 simplr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑢 ∈ ( Base ‘ 𝑉 ) )
34 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝒫 𝑌 = ( Base ‘ 𝑉 ) )
35 33 34 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑢 ∈ 𝒫 𝑌 )
36 35 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 ) → 𝑢 ∈ 𝒫 𝑌 )
37 36 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 ) → 𝑢 ⊆ 𝑌 )
38 37 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑗 ∈ 𝑢 ) → 𝑗 ∈ 𝑌 )
39 7 ffund ⊢ ( 𝜑 → Fun 𝐹 )
40 39 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑗 ∈ 𝑢 ) → Fun 𝐹 )
41 snssi ⊢ ( 𝑗 ∈ 𝑢 → { 𝑗 } ⊆ 𝑢 )
42 41 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑗 ∈ 𝑢 ) → { 𝑗 } ⊆ 𝑢 )
43 sspreima ⊢ ( ( Fun 𝐹 ∧ { 𝑗 } ⊆ 𝑢 ) → ( ◡ 𝐹 “ { 𝑗 } ) ⊆ ( ◡ 𝐹 “ 𝑢 ) )
44 40 42 43 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑗 ∈ 𝑢 ) → ( ◡ 𝐹 “ { 𝑗 } ) ⊆ ( ◡ 𝐹 “ 𝑢 ) )
45 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑗 ∈ 𝑢 ) → ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 )
46 44 45 sstrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑗 ∈ 𝑢 ) → ( ◡ 𝐹 “ { 𝑗 } ) ⊆ 𝑣 )
47 32 38 46 elrabd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑗 ∈ 𝑢 ) → 𝑗 ∈ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } )
48 47 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 ) → ( 𝑗 ∈ 𝑢 → 𝑗 ∈ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) )
49 48 ssrdv ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 ) → 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } )
50 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) ∧ 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) ) → 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } )
51 7 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
52 51 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) ∧ 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) ) → 𝐹 Fn 𝑋 )
53 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) ∧ 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) ) → 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) )
54 elpreima ⊢ ( 𝐹 Fn 𝑋 → ( 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) ↔ ( 𝑖 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑖 ) ∈ 𝑢 ) ) )
55 54 biimpa ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) ) → ( 𝑖 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑖 ) ∈ 𝑢 ) )
56 52 53 55 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) ∧ 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) ) → ( 𝑖 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑖 ) ∈ 𝑢 ) )
57 56 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) ∧ 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ 𝑢 )
58 50 57 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) ∧ 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } )
59 sneq ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑖 ) → { 𝑦 } = { ( 𝐹 ‘ 𝑖 ) } )
60 59 imaeq2d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑖 ) → ( ◡ 𝐹 “ { 𝑦 } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑖 ) } ) )
61 60 sseq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑖 ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 ↔ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑖 ) } ) ⊆ 𝑣 ) )
62 61 elrab ⊢ ( ( 𝐹 ‘ 𝑖 ) ∈ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ↔ ( ( 𝐹 ‘ 𝑖 ) ∈ 𝑌 ∧ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑖 ) } ) ⊆ 𝑣 ) )
63 62 simprbi ⊢ ( ( 𝐹 ‘ 𝑖 ) ∈ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑖 ) } ) ⊆ 𝑣 )
64 58 63 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) ∧ 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑖 ) } ) ⊆ 𝑣 )
65 56 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) ∧ 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) ) → 𝑖 ∈ 𝑋 )
66 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) ∧ 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) ) → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑖 ) )
67 fniniseg ⊢ ( 𝐹 Fn 𝑋 → ( 𝑖 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑖 ) } ) ↔ ( 𝑖 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑖 ) ) ) )
68 67 biimpar ⊢ ( ( 𝐹 Fn 𝑋 ∧ ( 𝑖 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑖 ) ) ) → 𝑖 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑖 ) } ) )
69 52 65 66 68 syl12anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) ∧ 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) ) → 𝑖 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑖 ) } ) )
70 64 69 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) ∧ 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) ) → 𝑖 ∈ 𝑣 )
71 70 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) → ( 𝑖 ∈ ( ◡ 𝐹 “ 𝑢 ) → 𝑖 ∈ 𝑣 ) )
72 71 ssrdv ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) → ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 )
73 49 72 impbida ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 ↔ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) )
74 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑛 = 𝑢 ) → 𝑛 = 𝑢 )
75 74 imaeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑛 = 𝑢 ) → ( ◡ 𝐹 “ 𝑛 ) = ( ◡ 𝐹 “ 𝑢 ) )
76 7 5 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
77 cnvexg ⊢ ( 𝐹 ∈ V → ◡ 𝐹 ∈ V )
78 imaexg ⊢ ( ◡ 𝐹 ∈ V → ( ◡ 𝐹 “ 𝑢 ) ∈ V )
79 76 77 78 3syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑢 ) ∈ V )
80 79 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ◡ 𝐹 “ 𝑢 ) ∈ V )
81 1 75 35 80 fvmptd2 ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐺 ‘ 𝑢 ) = ( ◡ 𝐹 “ 𝑢 ) )
82 81 sseq1d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐺 ‘ 𝑢 ) ⊆ 𝑣 ↔ ( ◡ 𝐹 “ 𝑢 ) ⊆ 𝑣 ) )
83 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑚 = 𝑣 ) → 𝑚 = 𝑣 )
84 83 sseq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑚 = 𝑣 ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑚 ↔ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 ) )
85 84 rabbidv ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑚 = 𝑣 ) → { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑚 } = { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } )
86 simpr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑣 ∈ ( Base ‘ 𝑊 ) )
87 5 17 syl ⊢ ( 𝜑 → 𝒫 𝑋 ∈ V )
88 87 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝒫 𝑋 ∈ V )
89 88 18 syl ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝒫 𝑋 = ( Base ‘ 𝑊 ) )
90 86 89 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑣 ∈ 𝒫 𝑋 )
91 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑌 ∈ 𝐵 )
92 ssrab2 ⊢ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ⊆ 𝑌
93 92 a1i ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ⊆ 𝑌 )
94 91 93 sselpwd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ∈ 𝒫 𝑌 )
95 2 85 90 94 fvmptd2 ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐻 ‘ 𝑣 ) = { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } )
96 95 sseq2d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑢 ⊆ ( 𝐻 ‘ 𝑣 ) ↔ 𝑢 ⊆ { 𝑦 ∈ 𝑌 ∣ ( ◡ 𝐹 “ { 𝑦 } ) ⊆ 𝑣 } ) )
97 73 82 96 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐺 ‘ 𝑢 ) ⊆ 𝑣 ↔ 𝑢 ⊆ ( 𝐻 ‘ 𝑣 ) ) )
98 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝐺 : 𝒫 𝑌 ⟶ 𝒫 𝑋 )
99 98 35 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐺 ‘ 𝑢 ) ∈ 𝒫 𝑋 )
100 eqid ⊢ ( le ‘ 𝑊 ) = ( le ‘ 𝑊 )
101 4 100 ipole ⊢ ( ( 𝒫 𝑋 ∈ V ∧ ( 𝐺 ‘ 𝑢 ) ∈ 𝒫 𝑋 ∧ 𝑣 ∈ 𝒫 𝑋 ) → ( ( 𝐺 ‘ 𝑢 ) ( le ‘ 𝑊 ) 𝑣 ↔ ( 𝐺 ‘ 𝑢 ) ⊆ 𝑣 ) )
102 88 99 90 101 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐺 ‘ 𝑢 ) ( le ‘ 𝑊 ) 𝑣 ↔ ( 𝐺 ‘ 𝑢 ) ⊆ 𝑣 ) )
103 6 14 syl ⊢ ( 𝜑 → 𝒫 𝑌 ∈ V )
104 103 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝒫 𝑌 ∈ V )
105 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝐻 : 𝒫 𝑋 ⟶ 𝒫 𝑌 )
106 105 90 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐻 ‘ 𝑣 ) ∈ 𝒫 𝑌 )
107 eqid ⊢ ( le ‘ 𝑉 ) = ( le ‘ 𝑉 )
108 3 107 ipole ⊢ ( ( 𝒫 𝑌 ∈ V ∧ 𝑢 ∈ 𝒫 𝑌 ∧ ( 𝐻 ‘ 𝑣 ) ∈ 𝒫 𝑌 ) → ( 𝑢 ( le ‘ 𝑉 ) ( 𝐻 ‘ 𝑣 ) ↔ 𝑢 ⊆ ( 𝐻 ‘ 𝑣 ) ) )
109 104 35 106 108 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑢 ( le ‘ 𝑉 ) ( 𝐻 ‘ 𝑣 ) ↔ 𝑢 ⊆ ( 𝐻 ‘ 𝑣 ) ) )
110 97 102 109 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( Base ‘ 𝑉 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐺 ‘ 𝑢 ) ( le ‘ 𝑊 ) 𝑣 ↔ 𝑢 ( le ‘ 𝑉 ) ( 𝐻 ‘ 𝑣 ) ) )
111 110 anasss ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑉 ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝐺 ‘ 𝑢 ) ( le ‘ 𝑊 ) 𝑣 ↔ 𝑢 ( le ‘ 𝑉 ) ( 𝐻 ‘ 𝑣 ) ) )
112 111 ralrimivva ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( Base ‘ 𝑉 ) ∀ 𝑣 ∈ ( Base ‘ 𝑊 ) ( ( 𝐺 ‘ 𝑢 ) ( le ‘ 𝑊 ) 𝑣 ↔ 𝑢 ( le ‘ 𝑉 ) ( 𝐻 ‘ 𝑣 ) ) )
113 eqid ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
114 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
115 eqid ⊢ ( 𝑉 MGalConn 𝑊 ) = ( 𝑉 MGalConn 𝑊 )
116 3 ipopos ⊢ 𝑉 ∈ Poset
117 posprs ⊢ ( 𝑉 ∈ Poset → 𝑉 ∈ Proset )
118 116 117 mp1i ⊢ ( 𝜑 → 𝑉 ∈ Proset )
119 4 ipopos ⊢ 𝑊 ∈ Poset
120 posprs ⊢ ( 𝑊 ∈ Poset → 𝑊 ∈ Proset )
121 119 120 mp1i ⊢ ( 𝜑 → 𝑊 ∈ Proset )
122 113 114 107 100 115 118 121 mgcval ⊢ ( 𝜑 → ( 𝐺 ( 𝑉 MGalConn 𝑊 ) 𝐻 ↔ ( ( 𝐺 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ∧ 𝐻 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑉 ) ∀ 𝑣 ∈ ( Base ‘ 𝑊 ) ( ( 𝐺 ‘ 𝑢 ) ( le ‘ 𝑊 ) 𝑣 ↔ 𝑢 ( le ‘ 𝑉 ) ( 𝐻 ‘ 𝑣 ) ) ) ) )
123 29 112 122 mpbir2and ⊢ ( 𝜑 → 𝐺 ( 𝑉 MGalConn 𝑊 ) 𝐻 )