Theorem dfmgc2lem 32811

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 510	. 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴))
4		mgcval.2	. . . . . . 7 ⊢ (𝜑 → 𝑉 ∈ Proset )
5	4	ad3antrrr 728	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑉 ∈ Proset )
6		simplr 767	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝑧 ∈ 𝐴)
7	6	adantr 479	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ∈ 𝐴)
8	2	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝐺:𝐵⟶𝐴)
9	1	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝐹:𝐴⟶𝐵)
10	9, 7	ffvelcdmd 7094	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐹‘𝑧) ∈ 𝐵)
11	8, 10	ffvelcdmd 7094	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘(𝐹‘𝑧)) ∈ 𝐴)
12	2	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝐺:𝐵⟶𝐴)
13		simpr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ 𝐵)
14	12, 13	ffvelcdmd 7094	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝐺‘𝑤) ∈ 𝐴)
15	14	adantr 479	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘𝑤) ∈ 𝐴)
16		dfmgc2lem.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
17	16	ralrimiva 3135	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
18	17	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
19		simpr 483	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → 𝑥 = 𝑧)
20	19	fveq2d 6900	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝐹‘𝑥) = (𝐹‘𝑧))
21	20	fveq2d 6900	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝐺‘(𝐹‘𝑥)) = (𝐺‘(𝐹‘𝑧)))
22	19, 21	breq12d 5162	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝑥 ≤ (𝐺‘(𝐹‘𝑥)) ↔ 𝑧 ≤ (𝐺‘(𝐹‘𝑧))))
23	7, 22	rspcdv 3598	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)) → 𝑧 ≤ (𝐺‘(𝐹‘𝑧))))
24	18, 23	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ≤ (𝐺‘(𝐹‘𝑧)))
25		dfmgc2lem.4	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))
26	25	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))
27		breq1 5152	. . . . . . . . . 10 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑢 ≲ 𝑣 ↔ (𝐹‘𝑧) ≲ 𝑣))
28		fveq2 6896	. . . . . . . . . . 11 ⊢ (𝑢 = (𝐹‘𝑧) → (𝐺‘𝑢) = (𝐺‘(𝐹‘𝑧)))
29	28	breq1d 5159	. . . . . . . . . 10 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝐺‘𝑢) ≤ (𝐺‘𝑣) ↔ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣)))
30	27, 29	imbi12d 343	. . . . . . . . 9 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)) ↔ ((𝐹‘𝑧) ≲ 𝑣 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣))))
31		breq2 5153	. . . . . . . . . 10 ⊢ (𝑣 = 𝑤 → ((𝐹‘𝑧) ≲ 𝑣 ↔ (𝐹‘𝑧) ≲ 𝑤))
32		fveq2 6896	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑤 → (𝐺‘𝑣) = (𝐺‘𝑤))
33	32	breq2d 5161	. . . . . . . . . 10 ⊢ (𝑣 = 𝑤 → ((𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣) ↔ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤)))
34	31, 33	imbi12d 343	. . . . . . . . 9 ⊢ (𝑣 = 𝑤 → (((𝐹‘𝑧) ≲ 𝑣 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣)) ↔ ((𝐹‘𝑧) ≲ 𝑤 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))))
35	1	ffvelcdmda 7093	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
36	35	adantr 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝐹‘𝑧) ∈ 𝐵)
37		eqidd 2726	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑢 = (𝐹‘𝑧)) → 𝐵 = 𝐵)
38	30, 34, 36, 37, 13	rspc2vd 3940	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)) → ((𝐹‘𝑧) ≲ 𝑤 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))))
39	26, 38	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ((𝐹‘𝑧) ≲ 𝑤 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤)))
40	39	imp 405	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))
41		mgcoval.1	. . . . . . 7 ⊢ 𝐴 = (Base‘𝑉)
42		mgcoval.3	. . . . . . 7 ⊢ ≤ = (le‘𝑉)
43	41, 42	prstr 18295	. . . . . 6 ⊢ ((𝑉 ∈ Proset ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘(𝐹‘𝑧)) ∈ 𝐴 ∧ (𝐺‘𝑤) ∈ 𝐴) ∧ (𝑧 ≤ (𝐺‘(𝐹‘𝑧)) ∧ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))) → 𝑧 ≤ (𝐺‘𝑤))
44	5, 7, 11, 15, 24, 40, 43	syl132anc 1385	. . . . 5 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ≤ (𝐺‘𝑤))
45		mgcval.3	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Proset )
46	45	ad3antrrr 728	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝑊 ∈ Proset )
47	35	ad2antrr 724	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ∈ 𝐵)
48	1	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝐹:𝐴⟶𝐵)
49	14	adantr 479	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐺‘𝑤) ∈ 𝐴)
50	48, 49	ffvelcdmd 7094	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘(𝐺‘𝑤)) ∈ 𝐵)
51		simplr 767	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝑤 ∈ 𝐵)
52		dfmgc2lem.3	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
53	52	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
54		breq1 5152	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 ≤ 𝑦 ↔ 𝑧 ≤ 𝑦))
55		fveq2 6896	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
56	55	breq1d 5159	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ≲ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ≲ (𝐹‘𝑦)))
57	54, 56	imbi12d 343	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ↔ (𝑧 ≤ 𝑦 → (𝐹‘𝑧) ≲ (𝐹‘𝑦))))
58		breq2 5153	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘𝑤) → (𝑧 ≤ 𝑦 ↔ 𝑧 ≤ (𝐺‘𝑤)))
59		fveq2 6896	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐺‘𝑤) → (𝐹‘𝑦) = (𝐹‘(𝐺‘𝑤)))
60	59	breq2d 5161	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘𝑤) → ((𝐹‘𝑧) ≲ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤))))
61	58, 60	imbi12d 343	. . . . . . . . 9 ⊢ (𝑦 = (𝐺‘𝑤) → ((𝑧 ≤ 𝑦 → (𝐹‘𝑧) ≲ (𝐹‘𝑦)) ↔ (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))))
62		eqidd 2726	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑥 = 𝑧) → 𝐴 = 𝐴)
63	57, 61, 6, 62, 14	rspc2vd 3940	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))))
64	53, 63	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤))))
65	64	imp 405	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))
66		dfmgc2lem.6	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
67	66	ralrimiva 3135	. . . . . . . 8 ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
68	67	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → ∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
69		simpr 483	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → 𝑢 = 𝑤)
70	69	fveq2d 6900	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → (𝐺‘𝑢) = (𝐺‘𝑤))
71	70	fveq2d 6900	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝑤)))
72	71, 69	breq12d 5162	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → ((𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ↔ (𝐹‘(𝐺‘𝑤)) ≲ 𝑤))
73	51, 72	rspcdv 3598	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 → (𝐹‘(𝐺‘𝑤)) ≲ 𝑤))
74	68, 73	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘(𝐺‘𝑤)) ≲ 𝑤)
75		mgcoval.2	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑊)
76		mgcoval.4	. . . . . . 7 ⊢ ≲ = (le‘𝑊)
77	75, 76	prstr 18295	. . . . . 6 ⊢ ((𝑊 ∈ Proset ∧ ((𝐹‘𝑧) ∈ 𝐵 ∧ (𝐹‘(𝐺‘𝑤)) ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ ((𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)) ∧ (𝐹‘(𝐺‘𝑤)) ≲ 𝑤)) → (𝐹‘𝑧) ≲ 𝑤)
78	46, 47, 50, 51, 65, 74, 77	syl132anc 1385	. . . . 5 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ≲ 𝑤)
79	44, 78	impbida 799	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
80	79	anasss 465	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
81	80	ralrimivva 3190	. 2 ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
82		mgcval.1	. . 3 ⊢ 𝐻 = (𝑉MGalConn𝑊)
83	41, 75, 42, 76, 82, 4, 45	mgcval 32803	. 2 ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))))
84	3, 81, 83	mpbir2and 711	1 ⊢ (𝜑 → 𝐹𝐻𝐺)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ∀wral 3050   class class class wbr 5149  ⟶wf 6545  ‘cfv 6549  (class class class)co 7419  Basecbs 17183  lecple 17243   Proset cproset 18288  MGalConncmgc 32795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-map 8847  df-proset 18290  df-mgc 32797

This theorem is referenced by:  dfmgc2  32812