Step | Hyp | Ref
| Expression |
1 | | mgcval.1 |
. . . 4
⊢ 𝐻 = (𝑉MGalConn𝑊) |
2 | | mgcval.2 |
. . . . 5
⊢ (𝜑 → 𝑉 ∈ Proset ) |
3 | | mgcval.3 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ Proset ) |
4 | | mgcoval.1 |
. . . . . 6
⊢ 𝐴 = (Base‘𝑉) |
5 | | mgcoval.2 |
. . . . . 6
⊢ 𝐵 = (Base‘𝑊) |
6 | | mgcoval.3 |
. . . . . 6
⊢ ≤ =
(le‘𝑉) |
7 | | mgcoval.4 |
. . . . . 6
⊢ ≲ =
(le‘𝑊) |
8 | 4, 5, 6, 7 | mgcoval 30655 |
. . . . 5
⊢ ((𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → (𝑉MGalConn𝑊) = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))}) |
9 | 2, 3, 8 | syl2anc 586 |
. . . 4
⊢ (𝜑 → (𝑉MGalConn𝑊) = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))}) |
10 | 1, 9 | syl5eq 2867 |
. . 3
⊢ (𝜑 → 𝐻 = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))}) |
11 | 10 | breqd 5053 |
. 2
⊢ (𝜑 → (𝐹𝐻𝐺 ↔ 𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))}𝐺)) |
12 | | fveq1 6645 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥)) |
13 | 12 | adantr 483 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘𝑥) = (𝐹‘𝑥)) |
14 | 13 | breq1d 5052 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓‘𝑥) ≲ 𝑦 ↔ (𝐹‘𝑥) ≲ 𝑦)) |
15 | | fveq1 6645 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝑔‘𝑦) = (𝐺‘𝑦)) |
16 | 15 | adantl 484 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑔‘𝑦) = (𝐺‘𝑦)) |
17 | 16 | breq2d 5054 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥 ≤ (𝑔‘𝑦) ↔ 𝑥 ≤ (𝐺‘𝑦))) |
18 | 14, 17 | bibi12d 348 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)) ↔ ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)))) |
19 | 18 | 2ralbidv 3186 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)))) |
20 | | eqid 2820 |
. . . 4
⊢
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))} = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))} |
21 | 19, 20 | brab2a 5620 |
. . 3
⊢ (𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))}𝐺 ↔ ((𝐹 ∈ (𝐵 ↑m 𝐴) ∧ 𝐺 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)))) |
22 | 5 | fvexi 6660 |
. . . . . 6
⊢ 𝐵 ∈ V |
23 | 4 | fvexi 6660 |
. . . . . 6
⊢ 𝐴 ∈ V |
24 | 22, 23 | elmap 8413 |
. . . . 5
⊢ (𝐹 ∈ (𝐵 ↑m 𝐴) ↔ 𝐹:𝐴⟶𝐵) |
25 | 23, 22 | elmap 8413 |
. . . . 5
⊢ (𝐺 ∈ (𝐴 ↑m 𝐵) ↔ 𝐺:𝐵⟶𝐴) |
26 | 24, 25 | anbi12i 628 |
. . . 4
⊢ ((𝐹 ∈ (𝐵 ↑m 𝐴) ∧ 𝐺 ∈ (𝐴 ↑m 𝐵)) ↔ (𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴)) |
27 | 26 | anbi1i 625 |
. . 3
⊢ (((𝐹 ∈ (𝐵 ↑m 𝐴) ∧ 𝐺 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦))) ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)))) |
28 | 21, 27 | bitr2i 278 |
. 2
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦))) ↔ 𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))}𝐺) |
29 | 11, 28 | syl6bbr 291 |
1
⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦))))) |