Step | Hyp | Ref
| Expression |
1 | | supsnti.ti |
. 2
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) |
2 | | supsnti.b |
. 2
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
3 | | snidg 3610 |
. . 3
⊢ (𝐵 ∈ 𝐴 → 𝐵 ∈ {𝐵}) |
4 | 2, 3 | syl 14 |
. 2
⊢ (𝜑 → 𝐵 ∈ {𝐵}) |
5 | | eqid 2170 |
. . . . . 6
⊢ 𝐵 = 𝐵 |
6 | 1 | ralrimivva 2552 |
. . . . . . 7
⊢ (𝜑 → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) |
7 | | eqeq1 2177 |
. . . . . . . . . 10
⊢ (𝑢 = 𝐵 → (𝑢 = 𝑣 ↔ 𝐵 = 𝑣)) |
8 | | breq1 3990 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝐵 → (𝑢𝑅𝑣 ↔ 𝐵𝑅𝑣)) |
9 | 8 | notbid 662 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝐵 → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝐵𝑅𝑣)) |
10 | | breq2 3991 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝐵 → (𝑣𝑅𝑢 ↔ 𝑣𝑅𝐵)) |
11 | 10 | notbid 662 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝐵 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝐵)) |
12 | 9, 11 | anbi12d 470 |
. . . . . . . . . 10
⊢ (𝑢 = 𝐵 → ((¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢) ↔ (¬ 𝐵𝑅𝑣 ∧ ¬ 𝑣𝑅𝐵))) |
13 | 7, 12 | bibi12d 234 |
. . . . . . . . 9
⊢ (𝑢 = 𝐵 → ((𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)) ↔ (𝐵 = 𝑣 ↔ (¬ 𝐵𝑅𝑣 ∧ ¬ 𝑣𝑅𝐵)))) |
14 | | eqeq2 2180 |
. . . . . . . . . 10
⊢ (𝑣 = 𝐵 → (𝐵 = 𝑣 ↔ 𝐵 = 𝐵)) |
15 | | breq2 3991 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐵 → (𝐵𝑅𝑣 ↔ 𝐵𝑅𝐵)) |
16 | 15 | notbid 662 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐵 → (¬ 𝐵𝑅𝑣 ↔ ¬ 𝐵𝑅𝐵)) |
17 | | breq1 3990 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐵 → (𝑣𝑅𝐵 ↔ 𝐵𝑅𝐵)) |
18 | 17 | notbid 662 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐵 → (¬ 𝑣𝑅𝐵 ↔ ¬ 𝐵𝑅𝐵)) |
19 | 16, 18 | anbi12d 470 |
. . . . . . . . . 10
⊢ (𝑣 = 𝐵 → ((¬ 𝐵𝑅𝑣 ∧ ¬ 𝑣𝑅𝐵) ↔ (¬ 𝐵𝑅𝐵 ∧ ¬ 𝐵𝑅𝐵))) |
20 | 14, 19 | bibi12d 234 |
. . . . . . . . 9
⊢ (𝑣 = 𝐵 → ((𝐵 = 𝑣 ↔ (¬ 𝐵𝑅𝑣 ∧ ¬ 𝑣𝑅𝐵)) ↔ (𝐵 = 𝐵 ↔ (¬ 𝐵𝑅𝐵 ∧ ¬ 𝐵𝑅𝐵)))) |
21 | 13, 20 | rspc2v 2847 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴) → (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)) → (𝐵 = 𝐵 ↔ (¬ 𝐵𝑅𝐵 ∧ ¬ 𝐵𝑅𝐵)))) |
22 | 2, 2, 21 | syl2anc 409 |
. . . . . . 7
⊢ (𝜑 → (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)) → (𝐵 = 𝐵 ↔ (¬ 𝐵𝑅𝐵 ∧ ¬ 𝐵𝑅𝐵)))) |
23 | 6, 22 | mpd 13 |
. . . . . 6
⊢ (𝜑 → (𝐵 = 𝐵 ↔ (¬ 𝐵𝑅𝐵 ∧ ¬ 𝐵𝑅𝐵))) |
24 | 5, 23 | mpbii 147 |
. . . . 5
⊢ (𝜑 → (¬ 𝐵𝑅𝐵 ∧ ¬ 𝐵𝑅𝐵)) |
25 | 24 | simpld 111 |
. . . 4
⊢ (𝜑 → ¬ 𝐵𝑅𝐵) |
26 | 25 | adantr 274 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ {𝐵}) → ¬ 𝐵𝑅𝐵) |
27 | | elsni 3599 |
. . . . . 6
⊢ (𝑥 ∈ {𝐵} → 𝑥 = 𝐵) |
28 | 27 | breq2d 3999 |
. . . . 5
⊢ (𝑥 ∈ {𝐵} → (𝐵𝑅𝑥 ↔ 𝐵𝑅𝐵)) |
29 | 28 | notbid 662 |
. . . 4
⊢ (𝑥 ∈ {𝐵} → (¬ 𝐵𝑅𝑥 ↔ ¬ 𝐵𝑅𝐵)) |
30 | 29 | adantl 275 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ {𝐵}) → (¬ 𝐵𝑅𝑥 ↔ ¬ 𝐵𝑅𝐵)) |
31 | 26, 30 | mpbird 166 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ {𝐵}) → ¬ 𝐵𝑅𝑥) |
32 | 1, 2, 4, 31 | supmaxti 6977 |
1
⊢ (𝜑 → sup({𝐵}, 𝐴, 𝑅) = 𝐵) |