Theorem dfmgc2lem 32970

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 511	. 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴))
4		mgcval.2	. . . . . . 7 ⊢ (𝜑 → 𝑉 ∈ Proset )
5	4	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑉 ∈ Proset )
6		simplr 769	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝑧 ∈ 𝐴)
7	6	adantr 480	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ∈ 𝐴)
8	2	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝐺:𝐵⟶𝐴)
9	1	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝐹:𝐴⟶𝐵)
10	9, 7	ffvelcdmd 7105	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐹‘𝑧) ∈ 𝐵)
11	8, 10	ffvelcdmd 7105	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘(𝐹‘𝑧)) ∈ 𝐴)
12	2	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝐺:𝐵⟶𝐴)
13		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ 𝐵)
14	12, 13	ffvelcdmd 7105	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝐺‘𝑤) ∈ 𝐴)
15	14	adantr 480	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘𝑤) ∈ 𝐴)
16		dfmgc2lem.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
17	16	ralrimiva 3144	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
18	17	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
19		simpr 484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → 𝑥 = 𝑧)
20	19	fveq2d 6911	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝐹‘𝑥) = (𝐹‘𝑧))
21	20	fveq2d 6911	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝐺‘(𝐹‘𝑥)) = (𝐺‘(𝐹‘𝑧)))
22	19, 21	breq12d 5161	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝑥 ≤ (𝐺‘(𝐹‘𝑥)) ↔ 𝑧 ≤ (𝐺‘(𝐹‘𝑧))))
23	7, 22	rspcdv 3614	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)) → 𝑧 ≤ (𝐺‘(𝐹‘𝑧))))
24	18, 23	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ≤ (𝐺‘(𝐹‘𝑧)))
25		dfmgc2lem.4	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))
26	25	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))
27		breq1 5151	. . . . . . . . . 10 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑢 ≲ 𝑣 ↔ (𝐹‘𝑧) ≲ 𝑣))
28		fveq2 6907	. . . . . . . . . . 11 ⊢ (𝑢 = (𝐹‘𝑧) → (𝐺‘𝑢) = (𝐺‘(𝐹‘𝑧)))
29	28	breq1d 5158	. . . . . . . . . 10 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝐺‘𝑢) ≤ (𝐺‘𝑣) ↔ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣)))
30	27, 29	imbi12d 344	. . . . . . . . 9 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)) ↔ ((𝐹‘𝑧) ≲ 𝑣 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣))))
31		breq2 5152	. . . . . . . . . 10 ⊢ (𝑣 = 𝑤 → ((𝐹‘𝑧) ≲ 𝑣 ↔ (𝐹‘𝑧) ≲ 𝑤))
32		fveq2 6907	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑤 → (𝐺‘𝑣) = (𝐺‘𝑤))
33	32	breq2d 5160	. . . . . . . . . 10 ⊢ (𝑣 = 𝑤 → ((𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣) ↔ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤)))
34	31, 33	imbi12d 344	. . . . . . . . 9 ⊢ (𝑣 = 𝑤 → (((𝐹‘𝑧) ≲ 𝑣 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣)) ↔ ((𝐹‘𝑧) ≲ 𝑤 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))))
35	1	ffvelcdmda 7104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
36	35	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝐹‘𝑧) ∈ 𝐵)
37		eqidd 2736	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑢 = (𝐹‘𝑧)) → 𝐵 = 𝐵)
38	30, 34, 36, 37, 13	rspc2vd 3959	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)) → ((𝐹‘𝑧) ≲ 𝑤 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))))
39	26, 38	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ((𝐹‘𝑧) ≲ 𝑤 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤)))
40	39	imp 406	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))
41		mgcoval.1	. . . . . . 7 ⊢ 𝐴 = (Base‘𝑉)
42		mgcoval.3	. . . . . . 7 ⊢ ≤ = (le‘𝑉)
43	41, 42	prstr 18357	. . . . . 6 ⊢ ((𝑉 ∈ Proset ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘(𝐹‘𝑧)) ∈ 𝐴 ∧ (𝐺‘𝑤) ∈ 𝐴) ∧ (𝑧 ≤ (𝐺‘(𝐹‘𝑧)) ∧ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))) → 𝑧 ≤ (𝐺‘𝑤))
44	5, 7, 11, 15, 24, 40, 43	syl132anc 1387	. . . . 5 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ≤ (𝐺‘𝑤))
45		mgcval.3	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Proset )
46	45	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝑊 ∈ Proset )
47	35	ad2antrr 726	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ∈ 𝐵)
48	1	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝐹:𝐴⟶𝐵)
49	14	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐺‘𝑤) ∈ 𝐴)
50	48, 49	ffvelcdmd 7105	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘(𝐺‘𝑤)) ∈ 𝐵)
51		simplr 769	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝑤 ∈ 𝐵)
52		dfmgc2lem.3	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
53	52	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
54		breq1 5151	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 ≤ 𝑦 ↔ 𝑧 ≤ 𝑦))
55		fveq2 6907	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
56	55	breq1d 5158	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ≲ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ≲ (𝐹‘𝑦)))
57	54, 56	imbi12d 344	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ↔ (𝑧 ≤ 𝑦 → (𝐹‘𝑧) ≲ (𝐹‘𝑦))))
58		breq2 5152	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘𝑤) → (𝑧 ≤ 𝑦 ↔ 𝑧 ≤ (𝐺‘𝑤)))
59		fveq2 6907	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐺‘𝑤) → (𝐹‘𝑦) = (𝐹‘(𝐺‘𝑤)))
60	59	breq2d 5160	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘𝑤) → ((𝐹‘𝑧) ≲ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤))))
61	58, 60	imbi12d 344	. . . . . . . . 9 ⊢ (𝑦 = (𝐺‘𝑤) → ((𝑧 ≤ 𝑦 → (𝐹‘𝑧) ≲ (𝐹‘𝑦)) ↔ (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))))
62		eqidd 2736	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑥 = 𝑧) → 𝐴 = 𝐴)
63	57, 61, 6, 62, 14	rspc2vd 3959	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))))
64	53, 63	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤))))
65	64	imp 406	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))
66		dfmgc2lem.6	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
67	66	ralrimiva 3144	. . . . . . . 8 ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
68	67	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → ∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
69		simpr 484	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → 𝑢 = 𝑤)
70	69	fveq2d 6911	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → (𝐺‘𝑢) = (𝐺‘𝑤))
71	70	fveq2d 6911	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝑤)))
72	71, 69	breq12d 5161	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → ((𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ↔ (𝐹‘(𝐺‘𝑤)) ≲ 𝑤))
73	51, 72	rspcdv 3614	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 → (𝐹‘(𝐺‘𝑤)) ≲ 𝑤))
74	68, 73	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘(𝐺‘𝑤)) ≲ 𝑤)
75		mgcoval.2	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑊)
76		mgcoval.4	. . . . . . 7 ⊢ ≲ = (le‘𝑊)
77	75, 76	prstr 18357	. . . . . 6 ⊢ ((𝑊 ∈ Proset ∧ ((𝐹‘𝑧) ∈ 𝐵 ∧ (𝐹‘(𝐺‘𝑤)) ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ ((𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)) ∧ (𝐹‘(𝐺‘𝑤)) ≲ 𝑤)) → (𝐹‘𝑧) ≲ 𝑤)
78	46, 47, 50, 51, 65, 74, 77	syl132anc 1387	. . . . 5 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ≲ 𝑤)
79	44, 78	impbida 801	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
80	79	anasss 466	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
81	80	ralrimivva 3200	. 2 ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
82		mgcval.1	. . 3 ⊢ 𝐻 = (𝑉MGalConn𝑊)
83	41, 75, 42, 76, 82, 4, 45	mgcval 32962	. 2 ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))))
84	3, 81, 83	mpbir2and 713	1 ⊢ (𝜑 → 𝐹𝐻𝐺)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∀wral 3059   class class class wbr 5148  ⟶wf 6559  ‘cfv 6563  (class class class)co 7431  Basecbs 17245  lecple 17305   Proset cproset 18350  MGalConncmgc 32954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8867  df-proset 18352  df-mgc 32956

This theorem is referenced by:  dfmgc2  32971