This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mgccole1

Description: An inequality for the kernel operator G o. F . (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 ⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
mgccole1.2 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
Assertion mgccole1 ( 𝜑 → 𝑋 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) )

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 mgccole1.2 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
10 1 2 3 4 5 6 7 mgcval ⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) ) )
11 8 10 mpbid ⊢ ( 𝜑 → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) )
12 11 simplld ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
13 12 9 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
14 2 4 prsref ⊢ ( ( 𝑊 ∈ Proset ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑋 ) )
15 7 13 14 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑋 ) )
16 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
17 16 breq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ ( 𝐹 ‘ 𝑋 ) ≲ 𝑦 ) )
18 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ↔ 𝑋 ≤ ( 𝐺 ‘ 𝑦 ) ) )
19 17 18 bibi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≲ 𝑦 ↔ 𝑋 ≤ ( 𝐺 ‘ 𝑦 ) ) ) )
20 19 ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ≲ 𝑦 ↔ 𝑋 ≤ ( 𝐺 ‘ 𝑦 ) ) ) )
21 11 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) )
22 20 21 9 rspcdva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ≲ 𝑦 ↔ 𝑋 ≤ ( 𝐺 ‘ 𝑦 ) ) )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑋 ) ) → 𝑦 = ( 𝐹 ‘ 𝑋 ) )
24 23 breq2d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑋 ) ≲ 𝑦 ↔ ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑋 ) ) )
25 23 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑋 ) ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) )
26 25 breq2d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑋 ) ) → ( 𝑋 ≤ ( 𝐺 ‘ 𝑦 ) ↔ 𝑋 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
27 24 26 bibi12d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) ≲ 𝑦 ↔ 𝑋 ≤ ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑋 ) ↔ 𝑋 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )
28 13 27 rspcdv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑋 ) ≲ 𝑦 ↔ 𝑋 ≤ ( 𝐺 ‘ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑋 ) ↔ 𝑋 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )
29 22 28 mpd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑋 ) ↔ 𝑋 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
30 15 29 mpbid ⊢ ( 𝜑 → 𝑋 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) )