Metamath Proof Explorer


Theorem mgccole2

Description: Inequality for the closure operator ( F o. G ) of the Galois connection H . (Contributed by Thierry Arnoux, 26-Apr-2024)

Ref Expression
Hypotheses mgcoval.1 𝐴 = ( Base ‘ 𝑉 )
mgcoval.2 𝐵 = ( Base ‘ 𝑊 )
mgcoval.3 = ( le ‘ 𝑉 )
mgcoval.4 = ( le ‘ 𝑊 )
mgcval.1 𝐻 = ( 𝑉 MGalConn 𝑊 )
mgcval.2 ( 𝜑𝑉 ∈ Proset )
mgcval.3 ( 𝜑𝑊 ∈ Proset )
mgccole.1 ( 𝜑𝐹 𝐻 𝐺 )
mgccole2.1 ( 𝜑𝑌𝐵 )
Assertion mgccole2 ( 𝜑 → ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑌 )

Proof

Step Hyp Ref Expression
1 mgcoval.1 𝐴 = ( Base ‘ 𝑉 )
2 mgcoval.2 𝐵 = ( Base ‘ 𝑊 )
3 mgcoval.3 = ( le ‘ 𝑉 )
4 mgcoval.4 = ( le ‘ 𝑊 )
5 mgcval.1 𝐻 = ( 𝑉 MGalConn 𝑊 )
6 mgcval.2 ( 𝜑𝑉 ∈ Proset )
7 mgcval.3 ( 𝜑𝑊 ∈ Proset )
8 mgccole.1 ( 𝜑𝐹 𝐻 𝐺 )
9 mgccole2.1 ( 𝜑𝑌𝐵 )
10 1 2 3 4 5 6 7 mgcval ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴𝐵𝐺 : 𝐵𝐴 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) ) ) )
11 8 10 mpbid ( 𝜑 → ( ( 𝐹 : 𝐴𝐵𝐺 : 𝐵𝐴 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) ) )
12 11 simplrd ( 𝜑𝐺 : 𝐵𝐴 )
13 12 9 ffvelrnd ( 𝜑 → ( 𝐺𝑌 ) ∈ 𝐴 )
14 1 3 prsref ( ( 𝑉 ∈ Proset ∧ ( 𝐺𝑌 ) ∈ 𝐴 ) → ( 𝐺𝑌 ) ( 𝐺𝑌 ) )
15 6 13 14 syl2anc ( 𝜑 → ( 𝐺𝑌 ) ( 𝐺𝑌 ) )
16 11 simprd ( 𝜑 → ∀ 𝑥𝐴𝑦𝐵 ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) )
17 fveq2 ( 𝑥 = ( 𝐺𝑌 ) → ( 𝐹𝑥 ) = ( 𝐹 ‘ ( 𝐺𝑌 ) ) )
18 17 breq1d ( 𝑥 = ( 𝐺𝑌 ) → ( ( 𝐹𝑥 ) 𝑦 ↔ ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑦 ) )
19 breq1 ( 𝑥 = ( 𝐺𝑌 ) → ( 𝑥 ( 𝐺𝑦 ) ↔ ( 𝐺𝑌 ) ( 𝐺𝑦 ) ) )
20 18 19 bibi12d ( 𝑥 = ( 𝐺𝑌 ) → ( ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) ↔ ( ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑦 ↔ ( 𝐺𝑌 ) ( 𝐺𝑦 ) ) ) )
21 20 adantl ( ( 𝜑𝑥 = ( 𝐺𝑌 ) ) → ( ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) ↔ ( ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑦 ↔ ( 𝐺𝑌 ) ( 𝐺𝑦 ) ) ) )
22 21 ralbidv ( ( 𝜑𝑥 = ( 𝐺𝑌 ) ) → ( ∀ 𝑦𝐵 ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) ↔ ∀ 𝑦𝐵 ( ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑦 ↔ ( 𝐺𝑌 ) ( 𝐺𝑦 ) ) ) )
23 13 22 rspcdv ( 𝜑 → ( ∀ 𝑥𝐴𝑦𝐵 ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) → ∀ 𝑦𝐵 ( ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑦 ↔ ( 𝐺𝑌 ) ( 𝐺𝑦 ) ) ) )
24 16 23 mpd ( 𝜑 → ∀ 𝑦𝐵 ( ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑦 ↔ ( 𝐺𝑌 ) ( 𝐺𝑦 ) ) )
25 simpr ( ( 𝜑𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
26 25 breq2d ( ( 𝜑𝑦 = 𝑌 ) → ( ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑦 ↔ ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑌 ) )
27 fveq2 ( 𝑦 = 𝑌 → ( 𝐺𝑦 ) = ( 𝐺𝑌 ) )
28 27 adantl ( ( 𝜑𝑦 = 𝑌 ) → ( 𝐺𝑦 ) = ( 𝐺𝑌 ) )
29 28 breq2d ( ( 𝜑𝑦 = 𝑌 ) → ( ( 𝐺𝑌 ) ( 𝐺𝑦 ) ↔ ( 𝐺𝑌 ) ( 𝐺𝑌 ) ) )
30 26 29 bibi12d ( ( 𝜑𝑦 = 𝑌 ) → ( ( ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑦 ↔ ( 𝐺𝑌 ) ( 𝐺𝑦 ) ) ↔ ( ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑌 ↔ ( 𝐺𝑌 ) ( 𝐺𝑌 ) ) ) )
31 9 30 rspcdv ( 𝜑 → ( ∀ 𝑦𝐵 ( ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑦 ↔ ( 𝐺𝑌 ) ( 𝐺𝑦 ) ) → ( ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑌 ↔ ( 𝐺𝑌 ) ( 𝐺𝑌 ) ) ) )
32 24 31 mpd ( 𝜑 → ( ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑌 ↔ ( 𝐺𝑌 ) ( 𝐺𝑌 ) ) )
33 15 32 mpbird ( 𝜑 → ( 𝐹 ‘ ( 𝐺𝑌 ) ) 𝑌 )