Theorem dfmgc2

Description: Alternate definition of the monotone Galois connection. (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 )
Assertion	dfmgc2	⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) ) )

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	1 2 3 4 5 6 7	mgcval	⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) ) )
9	8	simprbda	⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) )
10	6	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑉 ∈ Proset )
11	7	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑊 ∈ Proset )
12		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → 𝐹 𝐻 𝐺 )
13		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑥 ∈ 𝐴 )
14		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑦 ∈ 𝐴 )
15		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑥 ≤ 𝑦 )
16	1 2 3 4 5 10 11 12 13 14 15	mgcmnt1	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) )
17	16	ex	⊢ ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
18	17	anasss	⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
19	18	ralrimivva	⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
20	6	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → 𝑉 ∈ Proset )
21	7	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → 𝑊 ∈ Proset )
22		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → 𝐹 𝐻 𝐺 )
23		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → 𝑢 ∈ 𝐵 )
24		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → 𝑣 ∈ 𝐵 )
25		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → 𝑢 ≲ 𝑣 )
26	1 2 3 4 5 20 21 22 23 24 25	mgcmnt2	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) )
27	26	ex	⊢ ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
28	27	anasss	⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
29	28	ralrimivva	⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
30	19 29	jca	⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) )
31	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑉 ∈ Proset )
32	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑊 ∈ Proset )
33		simplr	⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) → 𝐹 𝐻 𝐺 )
34		simpr	⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
35	1 2 3 4 5 31 32 33 34	mgccole2	⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 )
36	35	ralrimiva	⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 )
37	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑉 ∈ Proset )
38	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑊 ∈ Proset )
39		simplr	⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐹 𝐻 𝐺 )
40		simpr	⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
41	1 2 3 4 5 37 38 39 40	mgccole1	⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
42	41	ralrimiva	⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
43	36 42	jca	⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
44	30 43	jca	⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
45	9 44	jca	⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
46	6	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑉 ∈ Proset )
47	7	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑊 ∈ Proset )
48		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) )
49	48	simpld	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
50	48	simprd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 𝐺 : 𝐵 ⟶ 𝐴 )
51		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) )
52	51	simpld	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
53		breq1	⊢ ( 𝑥 = 𝑚 → ( 𝑥 ≤ 𝑦 ↔ 𝑚 ≤ 𝑦 ) )
54		fveq2	⊢ ( 𝑥 = 𝑚 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑚 ) )
55	54	breq1d	⊢ ( 𝑥 = 𝑚 → ( ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
56	53 55	imbi12d	⊢ ( 𝑥 = 𝑚 → ( ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑚 ≤ 𝑦 → ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) )
57		breq2	⊢ ( 𝑦 = 𝑛 → ( 𝑚 ≤ 𝑦 ↔ 𝑚 ≤ 𝑛 ) )
58		fveq2	⊢ ( 𝑦 = 𝑛 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑛 ) )
59	58	breq2d	⊢ ( 𝑦 = 𝑛 → ( ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑛 ) ) )
60	57 59	imbi12d	⊢ ( 𝑦 = 𝑛 → ( ( 𝑚 ≤ 𝑦 → ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑚 ≤ 𝑛 → ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑛 ) ) ) )
61	56 60	cbvral2vw	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑚 ∈ 𝐴 ∀ 𝑛 ∈ 𝐴 ( 𝑚 ≤ 𝑛 → ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑛 ) ) )
62	52 61	sylib	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ∀ 𝑚 ∈ 𝐴 ∀ 𝑛 ∈ 𝐴 ( 𝑚 ≤ 𝑛 → ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑛 ) ) )
63	51	simprd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
64		breq1	⊢ ( 𝑢 = 𝑖 → ( 𝑢 ≲ 𝑣 ↔ 𝑖 ≲ 𝑣 ) )
65		fveq2	⊢ ( 𝑢 = 𝑖 → ( 𝐺 ‘ 𝑢 ) = ( 𝐺 ‘ 𝑖 ) )
66	65	breq1d	⊢ ( 𝑢 = 𝑖 → ( ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ↔ ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
67	64 66	imbi12d	⊢ ( 𝑢 = 𝑖 → ( ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ↔ ( 𝑖 ≲ 𝑣 → ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) )
68		breq2	⊢ ( 𝑣 = 𝑗 → ( 𝑖 ≲ 𝑣 ↔ 𝑖 ≲ 𝑗 ) )
69		fveq2	⊢ ( 𝑣 = 𝑗 → ( 𝐺 ‘ 𝑣 ) = ( 𝐺 ‘ 𝑗 ) )
70	69	breq2d	⊢ ( 𝑣 = 𝑗 → ( ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑣 ) ↔ ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑗 ) ) )
71	68 70	imbi12d	⊢ ( 𝑣 = 𝑗 → ( ( 𝑖 ≲ 𝑣 → ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ↔ ( 𝑖 ≲ 𝑗 → ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑗 ) ) ) )
72	67 71	cbvral2vw	⊢ ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ↔ ∀ 𝑖 ∈ 𝐵 ∀ 𝑗 ∈ 𝐵 ( 𝑖 ≲ 𝑗 → ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑗 ) ) )
73	63 72	sylib	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ∀ 𝑖 ∈ 𝐵 ∀ 𝑗 ∈ 𝐵 ( 𝑖 ≲ 𝑗 → ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑗 ) ) )
74		id	⊢ ( 𝑥 = 𝑚 → 𝑥 = 𝑚 )
75		2fveq3	⊢ ( 𝑥 = 𝑚 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑚 ) ) )
76	74 75	breq12d	⊢ ( 𝑥 = 𝑚 → ( 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ 𝑚 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
77		simplr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
78		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → 𝑚 ∈ 𝐴 )
79	76 77 78	rspcdva	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → 𝑚 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑚 ) ) )
80		2fveq3	⊢ ( 𝑢 = 𝑖 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑖 ) ) )
81		id	⊢ ( 𝑢 = 𝑖 → 𝑢 = 𝑖 )
82	80 81	breq12d	⊢ ( 𝑢 = 𝑖 → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑖 ) ) ≲ 𝑖 ) )
83		simpllr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑖 ∈ 𝐵 ) → ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 )
84		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑖 ∈ 𝐵 ) → 𝑖 ∈ 𝐵 )
85	82 83 84	rspcdva	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑖 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑖 ) ) ≲ 𝑖 )
86	1 2 3 4 5 46 47 49 50 62 73 79 85	dfmgc2lem	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 𝐹 𝐻 𝐺 )
87	86	anasss	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) → 𝐹 𝐻 𝐺 )
88	87	anasss	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) → 𝐹 𝐻 𝐺 )
89	88	anasss	⊢ ( ( 𝜑 ∧ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) ) → 𝐹 𝐻 𝐺 )
90	45 89	impbida	⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) ) )