Metamath Proof Explorer

Theorem mgcf1olem1

Description: Property of a Galois connection, lemma for mgcf1o . (Contributed by Thierry Arnoux, 26-Jul-2024)

Ref Expression
Hypotheses mgcf1o.h ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
mgcf1o.a ⊢ 𝐴 = ( Base ‘ 𝑉 )
mgcf1o.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
mgcf1o.1 ⊢ ≤ = ( le ‘ 𝑉 )
mgcf1o.2 ⊢ ≲ = ( le ‘ 𝑊 )
mgcf1o.v ⊢ ( 𝜑 → 𝑉 ∈ Poset )
mgcf1o.w ⊢ ( 𝜑 → 𝑊 ∈ Poset )
mgcf1o.f ⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
mgcf1olem1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
Assertion mgcf1olem1 ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( 𝐹 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 mgcf1o.h ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
2 mgcf1o.a ⊢ 𝐴 = ( Base ‘ 𝑉 )
3 mgcf1o.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
4 mgcf1o.1 ⊢ ≤ = ( le ‘ 𝑉 )
5 mgcf1o.2 ⊢ ≲ = ( le ‘ 𝑊 )
6 mgcf1o.v ⊢ ( 𝜑 → 𝑉 ∈ Poset )
7 mgcf1o.w ⊢ ( 𝜑 → 𝑊 ∈ Poset )
8 mgcf1o.f ⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
9 mgcf1olem1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
10 posprs ⊢ ( 𝑉 ∈ Poset → 𝑉 ∈ Proset )
11 6 10 syl ⊢ ( 𝜑 → 𝑉 ∈ Proset )
12 posprs ⊢ ( 𝑊 ∈ Poset → 𝑊 ∈ Proset )
13 7 12 syl ⊢ ( 𝜑 → 𝑊 ∈ Proset )
14 2 3 4 5 1 11 13 dfmgc2 ⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) ) )
15 8 14 mpbid ⊢ ( 𝜑 → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
16 15 simplld ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
17 15 simplrd ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
18 16 9 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
19 17 18 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ 𝐴 )
20 16 19 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ 𝐵 )
21 2 3 4 5 1 11 13 8 18 mgccole2 ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ≲ ( 𝐹 ‘ 𝑋 ) )
22 2 3 4 5 1 11 13 8 9 mgccole1 ⊢ ( 𝜑 → 𝑋 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) )
23 2 3 4 5 1 11 13 8 9 19 22 mgcmnt1 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
24 3 5 posasymb ⊢ ( ( 𝑊 ∈ Poset ∧ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ≲ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) ↔ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( 𝐹 ‘ 𝑋 ) ) )
25 24 biimpa ⊢ ( ( ( 𝑊 ∈ Poset ∧ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ≲ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( 𝐹 ‘ 𝑋 ) )
26 7 20 18 21 23 25 syl32anc ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( 𝐹 ‘ 𝑋 ) )