Step | Hyp | Ref
| Expression |
1 | | supiso.4 |
. . 3
⊢ (𝜑 → 𝑅 Or 𝐴) |
2 | | supiso.1 |
. . . 4
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) |
3 | | isoso 7157 |
. . . 4
⊢ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵)) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝜑 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵)) |
5 | 1, 4 | mpbid 235 |
. 2
⊢ (𝜑 → 𝑆 Or 𝐵) |
6 | | isof1o 7132 |
. . . 4
⊢ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐹:𝐴–1-1-onto→𝐵) |
7 | | f1of 6661 |
. . . 4
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) |
8 | 2, 6, 7 | 3syl 18 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
9 | | supisoex.3 |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) |
10 | 1, 9 | supcl 9074 |
. . 3
⊢ (𝜑 → sup(𝐶, 𝐴, 𝑅) ∈ 𝐴) |
11 | 8, 10 | ffvelrnd 6905 |
. 2
⊢ (𝜑 → (𝐹‘sup(𝐶, 𝐴, 𝑅)) ∈ 𝐵) |
12 | 1, 9 | supub 9075 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ 𝐶 → ¬ sup(𝐶, 𝐴, 𝑅)𝑅𝑢)) |
13 | 12 | ralrimiv 3104 |
. . . . 5
⊢ (𝜑 → ∀𝑢 ∈ 𝐶 ¬ sup(𝐶, 𝐴, 𝑅)𝑅𝑢) |
14 | 1, 9 | suplub 9076 |
. . . . . . 7
⊢ (𝜑 → ((𝑢 ∈ 𝐴 ∧ 𝑢𝑅sup(𝐶, 𝐴, 𝑅)) → ∃𝑧 ∈ 𝐶 𝑢𝑅𝑧)) |
15 | 14 | expd 419 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ 𝐴 → (𝑢𝑅sup(𝐶, 𝐴, 𝑅) → ∃𝑧 ∈ 𝐶 𝑢𝑅𝑧))) |
16 | 15 | ralrimiv 3104 |
. . . . 5
⊢ (𝜑 → ∀𝑢 ∈ 𝐴 (𝑢𝑅sup(𝐶, 𝐴, 𝑅) → ∃𝑧 ∈ 𝐶 𝑢𝑅𝑧)) |
17 | | supiso.2 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ⊆ 𝐴) |
18 | 2, 17 | supisolem 9089 |
. . . . . 6
⊢ ((𝜑 ∧ sup(𝐶, 𝐴, 𝑅) ∈ 𝐴) → ((∀𝑢 ∈ 𝐶 ¬ sup(𝐶, 𝐴, 𝑅)𝑅𝑢 ∧ ∀𝑢 ∈ 𝐴 (𝑢𝑅sup(𝐶, 𝐴, 𝑅) → ∃𝑧 ∈ 𝐶 𝑢𝑅𝑧)) ↔ (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ (𝐹‘sup(𝐶, 𝐴, 𝑅))𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆(𝐹‘sup(𝐶, 𝐴, 𝑅)) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣)))) |
19 | 10, 18 | mpdan 687 |
. . . . 5
⊢ (𝜑 → ((∀𝑢 ∈ 𝐶 ¬ sup(𝐶, 𝐴, 𝑅)𝑅𝑢 ∧ ∀𝑢 ∈ 𝐴 (𝑢𝑅sup(𝐶, 𝐴, 𝑅) → ∃𝑧 ∈ 𝐶 𝑢𝑅𝑧)) ↔ (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ (𝐹‘sup(𝐶, 𝐴, 𝑅))𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆(𝐹‘sup(𝐶, 𝐴, 𝑅)) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣)))) |
20 | 13, 16, 19 | mpbi2and 712 |
. . . 4
⊢ (𝜑 → (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ (𝐹‘sup(𝐶, 𝐴, 𝑅))𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆(𝐹‘sup(𝐶, 𝐴, 𝑅)) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣))) |
21 | 20 | simpld 498 |
. . 3
⊢ (𝜑 → ∀𝑤 ∈ (𝐹 “ 𝐶) ¬ (𝐹‘sup(𝐶, 𝐴, 𝑅))𝑆𝑤) |
22 | 21 | r19.21bi 3130 |
. 2
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐹 “ 𝐶)) → ¬ (𝐹‘sup(𝐶, 𝐴, 𝑅))𝑆𝑤) |
23 | 20 | simprd 499 |
. . . 4
⊢ (𝜑 → ∀𝑤 ∈ 𝐵 (𝑤𝑆(𝐹‘sup(𝐶, 𝐴, 𝑅)) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣)) |
24 | 23 | r19.21bi 3130 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (𝑤𝑆(𝐹‘sup(𝐶, 𝐴, 𝑅)) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣)) |
25 | 24 | impr 458 |
. 2
⊢ ((𝜑 ∧ (𝑤 ∈ 𝐵 ∧ 𝑤𝑆(𝐹‘sup(𝐶, 𝐴, 𝑅)))) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣) |
26 | 5, 11, 22, 25 | eqsupd 9073 |
1
⊢ (𝜑 → sup((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘sup(𝐶, 𝐴, 𝑅))) |