Theorem dfmgc2lem 33074

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 516	. 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴))
4		mgcval.2	. . . . . . 7 ⊢ (𝜑 → 𝑉 ∈ Proset )
5	4	ad3antrrr 736	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑉 ∈ Proset )
6		simplr 774	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝑧 ∈ 𝐴)
7	6	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ∈ 𝐴)
8	2	ad3antrrr 736	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝐺:𝐵⟶𝐴)
9	1	ad3antrrr 736	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝐹:𝐴⟶𝐵)
10	9, 7	ffvelcdmd 7026	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐹‘𝑧) ∈ 𝐵)
11	8, 10	ffvelcdmd 7026	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘(𝐹‘𝑧)) ∈ 𝐴)
12	2	ad2antrr 732	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝐺:𝐵⟶𝐴)
13		simpr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ 𝐵)
14	12, 13	ffvelcdmd 7026	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝐺‘𝑤) ∈ 𝐴)
15	14	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘𝑤) ∈ 𝐴)
16		dfmgc2lem.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
17	16	ralrimiva 3131	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
18	17	ad3antrrr 736	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
19		simpr 485	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → 𝑥 = 𝑧)
20	19	fveq2d 6831	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝐹‘𝑥) = (𝐹‘𝑧))
21	20	fveq2d 6831	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝐺‘(𝐹‘𝑥)) = (𝐺‘(𝐹‘𝑧)))
22	19, 21	breq12d 5085	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝑥 ≤ (𝐺‘(𝐹‘𝑥)) ↔ 𝑧 ≤ (𝐺‘(𝐹‘𝑧))))
23	7, 22	rspcdv 3552	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)) → 𝑧 ≤ (𝐺‘(𝐹‘𝑧))))
24	18, 23	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ≤ (𝐺‘(𝐹‘𝑧)))
25		dfmgc2lem.4	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))
26	25	ad2antrr 732	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))
27		breq1 5075	. . . . . . . . . 10 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑢 ≲ 𝑣 ↔ (𝐹‘𝑧) ≲ 𝑣))
28		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑢 = (𝐹‘𝑧) → (𝐺‘𝑢) = (𝐺‘(𝐹‘𝑧)))
29	28	breq1d 5082	. . . . . . . . . 10 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝐺‘𝑢) ≤ (𝐺‘𝑣) ↔ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣)))
30	27, 29	imbi12d 345	. . . . . . . . 9 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)) ↔ ((𝐹‘𝑧) ≲ 𝑣 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣))))
31		breq2 5076	. . . . . . . . . 10 ⊢ (𝑣 = 𝑤 → ((𝐹‘𝑧) ≲ 𝑣 ↔ (𝐹‘𝑧) ≲ 𝑤))
32		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑤 → (𝐺‘𝑣) = (𝐺‘𝑤))
33	32	breq2d 5084	. . . . . . . . . 10 ⊢ (𝑣 = 𝑤 → ((𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣) ↔ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤)))
34	31, 33	imbi12d 345	. . . . . . . . 9 ⊢ (𝑣 = 𝑤 → (((𝐹‘𝑧) ≲ 𝑣 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣)) ↔ ((𝐹‘𝑧) ≲ 𝑤 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))))
35	1	ffvelcdmda 7025	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
36	35	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝐹‘𝑧) ∈ 𝐵)
37		eqidd 2740	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑢 = (𝐹‘𝑧)) → 𝐵 = 𝐵)
38	30, 34, 36, 37, 13	rspc2vd 3879	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)) → ((𝐹‘𝑧) ≲ 𝑤 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))))
39	26, 38	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ((𝐹‘𝑧) ≲ 𝑤 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤)))
40	39	imp 407	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))
41		mgcoval.1	. . . . . . 7 ⊢ 𝐴 = (Base‘𝑉)
42		mgcoval.3	. . . . . . 7 ⊢ ≤ = (le‘𝑉)
43	41, 42	prstr 18256	. . . . . 6 ⊢ ((𝑉 ∈ Proset ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘(𝐹‘𝑧)) ∈ 𝐴 ∧ (𝐺‘𝑤) ∈ 𝐴) ∧ (𝑧 ≤ (𝐺‘(𝐹‘𝑧)) ∧ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))) → 𝑧 ≤ (𝐺‘𝑤))
44	5, 7, 11, 15, 24, 40, 43	syl132anc 1396	. . . . 5 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ≤ (𝐺‘𝑤))
45		mgcval.3	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Proset )
46	45	ad3antrrr 736	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝑊 ∈ Proset )
47	35	ad2antrr 732	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ∈ 𝐵)
48	1	ad3antrrr 736	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝐹:𝐴⟶𝐵)
49	14	adantr 481	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐺‘𝑤) ∈ 𝐴)
50	48, 49	ffvelcdmd 7026	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘(𝐺‘𝑤)) ∈ 𝐵)
51		simplr 774	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝑤 ∈ 𝐵)
52		dfmgc2lem.3	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
53	52	ad2antrr 732	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
54		breq1 5075	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 ≤ 𝑦 ↔ 𝑧 ≤ 𝑦))
55		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
56	55	breq1d 5082	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ≲ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ≲ (𝐹‘𝑦)))
57	54, 56	imbi12d 345	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ↔ (𝑧 ≤ 𝑦 → (𝐹‘𝑧) ≲ (𝐹‘𝑦))))
58		breq2 5076	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘𝑤) → (𝑧 ≤ 𝑦 ↔ 𝑧 ≤ (𝐺‘𝑤)))
59		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐺‘𝑤) → (𝐹‘𝑦) = (𝐹‘(𝐺‘𝑤)))
60	59	breq2d 5084	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘𝑤) → ((𝐹‘𝑧) ≲ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤))))
61	58, 60	imbi12d 345	. . . . . . . . 9 ⊢ (𝑦 = (𝐺‘𝑤) → ((𝑧 ≤ 𝑦 → (𝐹‘𝑧) ≲ (𝐹‘𝑦)) ↔ (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))))
62		eqidd 2740	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑥 = 𝑧) → 𝐴 = 𝐴)
63	57, 61, 6, 62, 14	rspc2vd 3879	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))))
64	53, 63	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤))))
65	64	imp 407	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))
66		dfmgc2lem.6	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
67	66	ralrimiva 3131	. . . . . . . 8 ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
68	67	ad3antrrr 736	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → ∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
69		simpr 485	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → 𝑢 = 𝑤)
70	69	fveq2d 6831	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → (𝐺‘𝑢) = (𝐺‘𝑤))
71	70	fveq2d 6831	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝑤)))
72	71, 69	breq12d 5085	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → ((𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ↔ (𝐹‘(𝐺‘𝑤)) ≲ 𝑤))
73	51, 72	rspcdv 3552	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 → (𝐹‘(𝐺‘𝑤)) ≲ 𝑤))
74	68, 73	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘(𝐺‘𝑤)) ≲ 𝑤)
75		mgcoval.2	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑊)
76		mgcoval.4	. . . . . . 7 ⊢ ≲ = (le‘𝑊)
77	75, 76	prstr 18256	. . . . . 6 ⊢ ((𝑊 ∈ Proset ∧ ((𝐹‘𝑧) ∈ 𝐵 ∧ (𝐹‘(𝐺‘𝑤)) ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ ((𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)) ∧ (𝐹‘(𝐺‘𝑤)) ≲ 𝑤)) → (𝐹‘𝑧) ≲ 𝑤)
78	46, 47, 50, 51, 65, 74, 77	syl132anc 1396	. . . . 5 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ≲ 𝑤)
79	44, 78	impbida 806	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
80	79	anasss 467	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
81	80	ralrimivva 3182	. 2 ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
82		mgcval.1	. . 3 ⊢ 𝐻 = (𝑉MGalConn𝑊)
83	41, 75, 42, 76, 82, 4, 45	mgcval 33066	. 2 ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))))
84	3, 81, 83	mpbir2and 719	1 ⊢ (𝜑 → 𝐹𝐻𝐺)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053   class class class wbr 5072  ⟶wf 6481  ‘cfv 6485  (class class class)co 7356  Basecbs 17170  lecple 17218   Proset cproset 18249  MGalConncmgc 33058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-map 8765  df-proset 18251  df-mgc 33060

This theorem is referenced by:  dfmgc2  33075