Theorem dfmgc2lem 33173

Description: Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.)

Hypotheses

Ref	Expression
mgcoval.1	⊢ 𝐴 = (Base‘𝑉)
mgcoval.2	⊢ 𝐵 = (Base‘𝑊)
mgcoval.3	⊢ ≤ = (le‘𝑉)
mgcoval.4	⊢ ≲ = (le‘𝑊)
mgcval.1	⊢ 𝐻 = (𝑉MGalConn𝑊)
mgcval.2	⊢ (𝜑 → 𝑉 ∈ Proset )
mgcval.3	⊢ (𝜑 → 𝑊 ∈ Proset )
dfmgc2lem.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
dfmgc2lem.2	⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
dfmgc2lem.3	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
dfmgc2lem.4	⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))
dfmgc2lem.5	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
dfmgc2lem.6	⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)

Assertion

Ref	Expression
dfmgc2lem	⊢ (𝜑 → 𝐹𝐻𝐺)

Distinct variable groups:   𝑣, ≤   𝑣, ≲   𝑣,𝐴,𝑥,𝑦   𝑣,𝐵,𝑥,𝑦   𝑣,𝑉,𝑥,𝑦   𝑣,𝑊,𝑥,𝑦   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦   𝑢, ≤ ,𝑣   𝑥, ≤ ,𝑦   𝑢, ≲   𝑥, ≲ ,𝑦   𝑢,𝐴   𝑢,𝐵   𝑢,𝐹,𝑣   𝑢,𝐺,𝑣   𝜑,𝑢   𝜑,𝑥

Allowed substitution hints:   𝜑(𝑦,𝑣)   𝐻(𝑥,𝑦,𝑣,𝑢)   𝑉(𝑢)   𝑊(𝑢)

Proof of Theorem dfmgc2lem

Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfmgc2lem.1	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		dfmgc2lem.2	. . 3 ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
3	1, 2	jca 519	. 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴))
4		mgcval.2	. . . . . . 7 ⊢ (𝜑 → 𝑉 ∈ Proset )
5	4	ad3antrrr 740	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑉 ∈ Proset )
6		simplr 778	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝑧 ∈ 𝐴)
7	6	adantr 484	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ∈ 𝐴)
8	2	ad3antrrr 740	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝐺:𝐵⟶𝐴)
9	1	ad3antrrr 740	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝐹:𝐴⟶𝐵)
10	9, 7	ffvelcdmd 7066	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐹‘𝑧) ∈ 𝐵)
11	8, 10	ffvelcdmd 7066	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘(𝐹‘𝑧)) ∈ 𝐴)
12	2	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝐺:𝐵⟶𝐴)
13		simpr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ 𝐵)
14	12, 13	ffvelcdmd 7066	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝐺‘𝑤) ∈ 𝐴)
15	14	adantr 484	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘𝑤) ∈ 𝐴)
16		dfmgc2lem.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
17	16	ralrimiva 3154	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
18	17	ad3antrrr 740	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
19		simpr 488	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → 𝑥 = 𝑧)
20	19	fveq2d 6871	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝐹‘𝑥) = (𝐹‘𝑧))
21	20	fveq2d 6871	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝐺‘(𝐹‘𝑥)) = (𝐺‘(𝐹‘𝑧)))
22	19, 21	breq12d 5113	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝑥 ≤ (𝐺‘(𝐹‘𝑥)) ↔ 𝑧 ≤ (𝐺‘(𝐹‘𝑧))))
23	7, 22	rspcdv 3573	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)) → 𝑧 ≤ (𝐺‘(𝐹‘𝑧))))
24	18, 23	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ≤ (𝐺‘(𝐹‘𝑧)))
25		dfmgc2lem.4	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))
26	25	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))
27		breq1 5103	. . . . . . . . . 10 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑢 ≲ 𝑣 ↔ (𝐹‘𝑧) ≲ 𝑣))
28		fveq2 6867	. . . . . . . . . . 11 ⊢ (𝑢 = (𝐹‘𝑧) → (𝐺‘𝑢) = (𝐺‘(𝐹‘𝑧)))
29	28	breq1d 5110	. . . . . . . . . 10 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝐺‘𝑢) ≤ (𝐺‘𝑣) ↔ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣)))
30	27, 29	imbi12d 346	. . . . . . . . 9 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)) ↔ ((𝐹‘𝑧) ≲ 𝑣 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣))))
31		breq2 5104	. . . . . . . . . 10 ⊢ (𝑣 = 𝑤 → ((𝐹‘𝑧) ≲ 𝑣 ↔ (𝐹‘𝑧) ≲ 𝑤))
32		fveq2 6867	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑤 → (𝐺‘𝑣) = (𝐺‘𝑤))
33	32	breq2d 5112	. . . . . . . . . 10 ⊢ (𝑣 = 𝑤 → ((𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣) ↔ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤)))
34	31, 33	imbi12d 346	. . . . . . . . 9 ⊢ (𝑣 = 𝑤 → (((𝐹‘𝑧) ≲ 𝑣 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣)) ↔ ((𝐹‘𝑧) ≲ 𝑤 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))))
35	1	ffvelcdmda 7065	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
36	35	adantr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝐹‘𝑧) ∈ 𝐵)
37		eqidd 2763	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑢 = (𝐹‘𝑧)) → 𝐵 = 𝐵)
38	30, 34, 36, 37, 13	rspc2vd 3900	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)) → ((𝐹‘𝑧) ≲ 𝑤 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))))
39	26, 38	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ((𝐹‘𝑧) ≲ 𝑤 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤)))
40	39	imp 410	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))
41		mgcoval.1	. . . . . . 7 ⊢ 𝐴 = (Base‘𝑉)
42		mgcoval.3	. . . . . . 7 ⊢ ≤ = (le‘𝑉)
43	41, 42	prstr 18331	. . . . . 6 ⊢ ((𝑉 ∈ Proset ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘(𝐹‘𝑧)) ∈ 𝐴 ∧ (𝐺‘𝑤) ∈ 𝐴) ∧ (𝑧 ≤ (𝐺‘(𝐹‘𝑧)) ∧ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))) → 𝑧 ≤ (𝐺‘𝑤))
44	5, 7, 11, 15, 24, 40, 43	syl132anc 1407	. . . . 5 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ≤ (𝐺‘𝑤))
45		mgcval.3	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Proset )
46	45	ad3antrrr 740	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝑊 ∈ Proset )
47	35	ad2antrr 736	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ∈ 𝐵)
48	1	ad3antrrr 740	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝐹:𝐴⟶𝐵)
49	14	adantr 484	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐺‘𝑤) ∈ 𝐴)
50	48, 49	ffvelcdmd 7066	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘(𝐺‘𝑤)) ∈ 𝐵)
51		simplr 778	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝑤 ∈ 𝐵)
52		dfmgc2lem.3	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
53	52	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
54		breq1 5103	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 ≤ 𝑦 ↔ 𝑧 ≤ 𝑦))
55		fveq2 6867	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
56	55	breq1d 5110	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ≲ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ≲ (𝐹‘𝑦)))
57	54, 56	imbi12d 346	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ↔ (𝑧 ≤ 𝑦 → (𝐹‘𝑧) ≲ (𝐹‘𝑦))))
58		breq2 5104	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘𝑤) → (𝑧 ≤ 𝑦 ↔ 𝑧 ≤ (𝐺‘𝑤)))
59		fveq2 6867	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐺‘𝑤) → (𝐹‘𝑦) = (𝐹‘(𝐺‘𝑤)))
60	59	breq2d 5112	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘𝑤) → ((𝐹‘𝑧) ≲ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤))))
61	58, 60	imbi12d 346	. . . . . . . . 9 ⊢ (𝑦 = (𝐺‘𝑤) → ((𝑧 ≤ 𝑦 → (𝐹‘𝑧) ≲ (𝐹‘𝑦)) ↔ (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))))
62		eqidd 2763	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑥 = 𝑧) → 𝐴 = 𝐴)
63	57, 61, 6, 62, 14	rspc2vd 3900	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))))
64	53, 63	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤))))
65	64	imp 410	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))
66		dfmgc2lem.6	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
67	66	ralrimiva 3154	. . . . . . . 8 ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
68	67	ad3antrrr 740	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → ∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
69		simpr 488	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → 𝑢 = 𝑤)
70	69	fveq2d 6871	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → (𝐺‘𝑢) = (𝐺‘𝑤))
71	70	fveq2d 6871	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝑤)))
72	71, 69	breq12d 5113	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → ((𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ↔ (𝐹‘(𝐺‘𝑤)) ≲ 𝑤))
73	51, 72	rspcdv 3573	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 → (𝐹‘(𝐺‘𝑤)) ≲ 𝑤))
74	68, 73	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘(𝐺‘𝑤)) ≲ 𝑤)
75		mgcoval.2	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑊)
76		mgcoval.4	. . . . . . 7 ⊢ ≲ = (le‘𝑊)
77	75, 76	prstr 18331	. . . . . 6 ⊢ ((𝑊 ∈ Proset ∧ ((𝐹‘𝑧) ∈ 𝐵 ∧ (𝐹‘(𝐺‘𝑤)) ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ ((𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)) ∧ (𝐹‘(𝐺‘𝑤)) ≲ 𝑤)) → (𝐹‘𝑧) ≲ 𝑤)
78	46, 47, 50, 51, 65, 74, 77	syl132anc 1407	. . . . 5 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ≲ 𝑤)
79	44, 78	impbida 810	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
80	79	anasss 470	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
81	80	ralrimivva 3205	. 2 ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
82		mgcval.1	. . 3 ⊢ 𝐻 = (𝑉MGalConn𝑊)
83	41, 75, 42, 76, 82, 4, 45	mgcval 33165	. 2 ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))))
84	3, 81, 83	mpbir2and 723	1 ⊢ (𝜑 → 𝐹𝐻𝐺)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ∀wral 3076   class class class wbr 5100  ⟶wf 6517  ‘cfv 6521  (class class class)co 7396  Basecbs 17245  lecple 17293   Proset cproset 18324  MGalConncmgc 33157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-map 8810  df-proset 18326  df-mgc 33159

This theorem is referenced by:  dfmgc2  33174