Theorem dfmgc2lem 33055

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 731	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑉 ∈ Proset )
6		simplr 769	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝑧 ∈ 𝐴)
7	6	adantr 480	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ∈ 𝐴)
8	2	ad3antrrr 731	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝐺:𝐵⟶𝐴)
9	1	ad3antrrr 731	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝐹:𝐴⟶𝐵)
10	9, 7	ffvelcdmd 7037	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐹‘𝑧) ∈ 𝐵)
11	8, 10	ffvelcdmd 7037	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘(𝐹‘𝑧)) ∈ 𝐴)
12	2	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝐺:𝐵⟶𝐴)
13		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ 𝐵)
14	12, 13	ffvelcdmd 7037	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝐺‘𝑤) ∈ 𝐴)
15	14	adantr 480	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (𝐺‘𝑤) ∈ 𝐴)
16		dfmgc2lem.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
17	16	ralrimiva 3129	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
18	17	ad3antrrr 731	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))
19		simpr 484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → 𝑥 = 𝑧)
20	19	fveq2d 6844	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝐹‘𝑥) = (𝐹‘𝑧))
21	20	fveq2d 6844	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝐺‘(𝐹‘𝑥)) = (𝐺‘(𝐹‘𝑧)))
22	19, 21	breq12d 5098	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) ∧ 𝑥 = 𝑧) → (𝑥 ≤ (𝐺‘(𝐹‘𝑥)) ↔ 𝑧 ≤ (𝐺‘(𝐹‘𝑧))))
23	7, 22	rspcdv 3556	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → (∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)) → 𝑧 ≤ (𝐺‘(𝐹‘𝑧))))
24	18, 23	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ≤ (𝐺‘(𝐹‘𝑧)))
25		dfmgc2lem.4	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))
26	25	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))
27		breq1 5088	. . . . . . . . . 10 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑢 ≲ 𝑣 ↔ (𝐹‘𝑧) ≲ 𝑣))
28		fveq2 6840	. . . . . . . . . . 11 ⊢ (𝑢 = (𝐹‘𝑧) → (𝐺‘𝑢) = (𝐺‘(𝐹‘𝑧)))
29	28	breq1d 5095	. . . . . . . . . 10 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝐺‘𝑢) ≤ (𝐺‘𝑣) ↔ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣)))
30	27, 29	imbi12d 344	. . . . . . . . 9 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)) ↔ ((𝐹‘𝑧) ≲ 𝑣 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣))))
31		breq2 5089	. . . . . . . . . 10 ⊢ (𝑣 = 𝑤 → ((𝐹‘𝑧) ≲ 𝑣 ↔ (𝐹‘𝑧) ≲ 𝑤))
32		fveq2 6840	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑤 → (𝐺‘𝑣) = (𝐺‘𝑤))
33	32	breq2d 5097	. . . . . . . . . 10 ⊢ (𝑣 = 𝑤 → ((𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣) ↔ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤)))
34	31, 33	imbi12d 344	. . . . . . . . 9 ⊢ (𝑣 = 𝑤 → (((𝐹‘𝑧) ≲ 𝑣 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑣)) ↔ ((𝐹‘𝑧) ≲ 𝑤 → (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))))
35	1	ffvelcdmda 7036	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
36	35	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝐹‘𝑧) ∈ 𝐵)
37		eqidd 2737	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑢 = (𝐹‘𝑧)) → 𝐵 = 𝐵)
38	30, 34, 36, 37, 13	rspc2vd 3885	. . . . . . . 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 18265	. . . . . 6 ⊢ ((𝑉 ∈ Proset ∧ (𝑧 ∈ 𝐴 ∧ (𝐺‘(𝐹‘𝑧)) ∈ 𝐴 ∧ (𝐺‘𝑤) ∈ 𝐴) ∧ (𝑧 ≤ (𝐺‘(𝐹‘𝑧)) ∧ (𝐺‘(𝐹‘𝑧)) ≤ (𝐺‘𝑤))) → 𝑧 ≤ (𝐺‘𝑤))
44	5, 7, 11, 15, 24, 40, 43	syl132anc 1391	. . . . 5 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ (𝐹‘𝑧) ≲ 𝑤) → 𝑧 ≤ (𝐺‘𝑤))
45		mgcval.3	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Proset )
46	45	ad3antrrr 731	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝑊 ∈ Proset )
47	35	ad2antrr 727	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ∈ 𝐵)
48	1	ad3antrrr 731	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝐹:𝐴⟶𝐵)
49	14	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐺‘𝑤) ∈ 𝐴)
50	48, 49	ffvelcdmd 7037	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘(𝐺‘𝑤)) ∈ 𝐵)
51		simplr 769	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → 𝑤 ∈ 𝐵)
52		dfmgc2lem.3	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
53	52	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))
54		breq1 5088	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 ≤ 𝑦 ↔ 𝑧 ≤ 𝑦))
55		fveq2 6840	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
56	55	breq1d 5095	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) ≲ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ≲ (𝐹‘𝑦)))
57	54, 56	imbi12d 344	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ↔ (𝑧 ≤ 𝑦 → (𝐹‘𝑧) ≲ (𝐹‘𝑦))))
58		breq2 5089	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘𝑤) → (𝑧 ≤ 𝑦 ↔ 𝑧 ≤ (𝐺‘𝑤)))
59		fveq2 6840	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐺‘𝑤) → (𝐹‘𝑦) = (𝐹‘(𝐺‘𝑤)))
60	59	breq2d 5097	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘𝑤) → ((𝐹‘𝑧) ≲ (𝐹‘𝑦) ↔ (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤))))
61	58, 60	imbi12d 344	. . . . . . . . 9 ⊢ (𝑦 = (𝐺‘𝑤) → ((𝑧 ≤ 𝑦 → (𝐹‘𝑧) ≲ (𝐹‘𝑦)) ↔ (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))))
62		eqidd 2737	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑥 = 𝑧) → 𝐴 = 𝐴)
63	57, 61, 6, 62, 14	rspc2vd 3885	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) → (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))))
64	53, 63	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝑧 ≤ (𝐺‘𝑤) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤))))
65	64	imp 406	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)))
66		dfmgc2lem.6	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
67	66	ralrimiva 3129	. . . . . . . 8 ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
68	67	ad3antrrr 731	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → ∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)
69		simpr 484	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → 𝑢 = 𝑤)
70	69	fveq2d 6844	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → (𝐺‘𝑢) = (𝐺‘𝑤))
71	70	fveq2d 6844	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝑤)))
72	71, 69	breq12d 5098	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) ∧ 𝑢 = 𝑤) → ((𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ↔ (𝐹‘(𝐺‘𝑤)) ≲ 𝑤))
73	51, 72	rspcdv 3556	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 → (𝐹‘(𝐺‘𝑤)) ≲ 𝑤))
74	68, 73	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘(𝐺‘𝑤)) ≲ 𝑤)
75		mgcoval.2	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑊)
76		mgcoval.4	. . . . . . 7 ⊢ ≲ = (le‘𝑊)
77	75, 76	prstr 18265	. . . . . 6 ⊢ ((𝑊 ∈ Proset ∧ ((𝐹‘𝑧) ∈ 𝐵 ∧ (𝐹‘(𝐺‘𝑤)) ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ ((𝐹‘𝑧) ≲ (𝐹‘(𝐺‘𝑤)) ∧ (𝐹‘(𝐺‘𝑤)) ≲ 𝑤)) → (𝐹‘𝑧) ≲ 𝑤)
78	46, 47, 50, 51, 65, 74, 77	syl132anc 1391	. . . . 5 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ≤ (𝐺‘𝑤)) → (𝐹‘𝑧) ≲ 𝑤)
79	44, 78	impbida 801	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
80	79	anasss 466	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
81	80	ralrimivva 3180	. 2 ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))
82		mgcval.1	. . 3 ⊢ 𝐻 = (𝑉MGalConn𝑊)
83	41, 75, 42, 76, 82, 4, 45	mgcval 33047	. 2 ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 ((𝐹‘𝑧) ≲ 𝑤 ↔ 𝑧 ≤ (𝐺‘𝑤)))))
84	3, 81, 83	mpbir2and 714	1 ⊢ (𝜑 → 𝐹𝐻𝐺)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3051   class class class wbr 5085  ⟶wf 6494  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  lecple 17227   Proset cproset 18258  MGalConncmgc 33039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-map 8775  df-proset 18260  df-mgc 33041

This theorem is referenced by:  dfmgc2  33056