Proof of Theorem suplem2pr
Step | Hyp | Ref
| Expression |
1 | | ltrelpr 10498 |
. . . . . 6
⊢
<P ⊆ (P ×
P) |
2 | 1 | brel 5588 |
. . . . 5
⊢ (𝑦<P
∪ 𝐴 → (𝑦 ∈ P ∧ ∪ 𝐴
∈ P)) |
3 | 2 | simpld 498 |
. . . 4
⊢ (𝑦<P
∪ 𝐴 → 𝑦 ∈ P) |
4 | | ralnex 3149 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝐴 ¬ 𝑦<P 𝑧 ↔ ¬ ∃𝑧 ∈ 𝐴 𝑦<P 𝑧) |
5 | | ssel2 3872 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ P ∧
𝑧 ∈ 𝐴) → 𝑧 ∈ P) |
6 | | ltsopr 10532 |
. . . . . . . . . . . . . . . 16
⊢
<P Or P |
7 | | sotric 5470 |
. . . . . . . . . . . . . . . 16
⊢
((<P Or P ∧ (𝑦 ∈ P ∧
𝑧 ∈ P))
→ (𝑦<P 𝑧 ↔ ¬ (𝑦 = 𝑧 ∨ 𝑧<P 𝑦))) |
8 | 6, 7 | mpan 690 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (𝑦<P 𝑧 ↔ ¬ (𝑦 = 𝑧 ∨ 𝑧<P 𝑦))) |
9 | 8 | con2bid 358 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ ((𝑦 = 𝑧 ∨ 𝑧<P 𝑦) ↔ ¬ 𝑦<P
𝑧)) |
10 | 9 | ancoms 462 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ P ∧
𝑦 ∈ P)
→ ((𝑦 = 𝑧 ∨ 𝑧<P 𝑦) ↔ ¬ 𝑦<P
𝑧)) |
11 | | ltprord 10530 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ P ∧
𝑦 ∈ P)
→ (𝑧<P 𝑦 ↔ 𝑧 ⊊ 𝑦)) |
12 | 11 | orbi2d 915 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ P ∧
𝑦 ∈ P)
→ ((𝑦 = 𝑧 ∨ 𝑧<P 𝑦) ↔ (𝑦 = 𝑧 ∨ 𝑧 ⊊ 𝑦))) |
13 | | sspss 3990 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ⊆ 𝑦 ↔ (𝑧 ⊊ 𝑦 ∨ 𝑧 = 𝑦)) |
14 | | equcom 2030 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑦 ↔ 𝑦 = 𝑧) |
15 | 14 | orbi2i 912 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ⊊ 𝑦 ∨ 𝑧 = 𝑦) ↔ (𝑧 ⊊ 𝑦 ∨ 𝑦 = 𝑧)) |
16 | | orcom 869 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ⊊ 𝑦 ∨ 𝑦 = 𝑧) ↔ (𝑦 = 𝑧 ∨ 𝑧 ⊊ 𝑦)) |
17 | 13, 15, 16 | 3bitri 300 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ⊆ 𝑦 ↔ (𝑦 = 𝑧 ∨ 𝑧 ⊊ 𝑦)) |
18 | 12, 17 | bitr4di 292 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ P ∧
𝑦 ∈ P)
→ ((𝑦 = 𝑧 ∨ 𝑧<P 𝑦) ↔ 𝑧 ⊆ 𝑦)) |
19 | 10, 18 | bitr3d 284 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ P ∧
𝑦 ∈ P)
→ (¬ 𝑦<P 𝑧 ↔ 𝑧 ⊆ 𝑦)) |
20 | 5, 19 | sylan 583 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ P ∧
𝑧 ∈ 𝐴) ∧ 𝑦 ∈ P) → (¬ 𝑦<P
𝑧 ↔ 𝑧 ⊆ 𝑦)) |
21 | 20 | an32s 652 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ P ∧
𝑦 ∈ P)
∧ 𝑧 ∈ 𝐴) → (¬ 𝑦<P
𝑧 ↔ 𝑧 ⊆ 𝑦)) |
22 | 21 | ralbidva 3108 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ P ∧
𝑦 ∈ P)
→ (∀𝑧 ∈
𝐴 ¬ 𝑦<P 𝑧 ↔ ∀𝑧 ∈ 𝐴 𝑧 ⊆ 𝑦)) |
23 | 4, 22 | bitr3id 288 |
. . . . . . . 8
⊢ ((𝐴 ⊆ P ∧
𝑦 ∈ P)
→ (¬ ∃𝑧
∈ 𝐴 𝑦<P 𝑧 ↔ ∀𝑧 ∈ 𝐴 𝑧 ⊆ 𝑦)) |
24 | | unissb 4830 |
. . . . . . . 8
⊢ (∪ 𝐴
⊆ 𝑦 ↔
∀𝑧 ∈ 𝐴 𝑧 ⊆ 𝑦) |
25 | 23, 24 | bitr4di 292 |
. . . . . . 7
⊢ ((𝐴 ⊆ P ∧
𝑦 ∈ P)
→ (¬ ∃𝑧
∈ 𝐴 𝑦<P 𝑧 ↔ ∪ 𝐴
⊆ 𝑦)) |
26 | | ssnpss 3994 |
. . . . . . . 8
⊢ (∪ 𝐴
⊆ 𝑦 → ¬
𝑦 ⊊ ∪ 𝐴) |
27 | | ltprord 10530 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ P ∧
∪ 𝐴 ∈ P) → (𝑦<P
∪ 𝐴 ↔ 𝑦 ⊊ ∪ 𝐴)) |
28 | 27 | biimpd 232 |
. . . . . . . . 9
⊢ ((𝑦 ∈ P ∧
∪ 𝐴 ∈ P) → (𝑦<P
∪ 𝐴 → 𝑦 ⊊ ∪ 𝐴)) |
29 | 2, 28 | mpcom 38 |
. . . . . . . 8
⊢ (𝑦<P
∪ 𝐴 → 𝑦 ⊊ ∪ 𝐴) |
30 | 26, 29 | nsyl 142 |
. . . . . . 7
⊢ (∪ 𝐴
⊆ 𝑦 → ¬
𝑦<P ∪ 𝐴) |
31 | 25, 30 | syl6bi 256 |
. . . . . 6
⊢ ((𝐴 ⊆ P ∧
𝑦 ∈ P)
→ (¬ ∃𝑧
∈ 𝐴 𝑦<P 𝑧 → ¬ 𝑦<P ∪ 𝐴)) |
32 | 31 | con4d 115 |
. . . . 5
⊢ ((𝐴 ⊆ P ∧
𝑦 ∈ P)
→ (𝑦<P ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑦<P 𝑧)) |
33 | 32 | ex 416 |
. . . 4
⊢ (𝐴 ⊆ P →
(𝑦 ∈ P
→ (𝑦<P ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑦<P 𝑧))) |
34 | 3, 33 | syl5 34 |
. . 3
⊢ (𝐴 ⊆ P →
(𝑦<P ∪ 𝐴
→ (𝑦<P ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑦<P 𝑧))) |
35 | 34 | pm2.43d 53 |
. 2
⊢ (𝐴 ⊆ P →
(𝑦<P ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑦<P 𝑧)) |
36 | | elssuni 4828 |
. . . 4
⊢ (𝑦 ∈ 𝐴 → 𝑦 ⊆ ∪ 𝐴) |
37 | | ssnpss 3994 |
. . . 4
⊢ (𝑦 ⊆ ∪ 𝐴
→ ¬ ∪ 𝐴 ⊊ 𝑦) |
38 | 36, 37 | syl 17 |
. . 3
⊢ (𝑦 ∈ 𝐴 → ¬ ∪
𝐴 ⊊ 𝑦) |
39 | 1 | brel 5588 |
. . . 4
⊢ (∪ 𝐴<P 𝑦 → (∪ 𝐴
∈ P ∧ 𝑦 ∈ P)) |
40 | | ltprord 10530 |
. . . . 5
⊢ ((∪ 𝐴
∈ P ∧ 𝑦 ∈ P) → (∪ 𝐴<P 𝑦 ↔ ∪ 𝐴
⊊ 𝑦)) |
41 | 40 | biimpd 232 |
. . . 4
⊢ ((∪ 𝐴
∈ P ∧ 𝑦 ∈ P) → (∪ 𝐴<P 𝑦 → ∪ 𝐴
⊊ 𝑦)) |
42 | 39, 41 | mpcom 38 |
. . 3
⊢ (∪ 𝐴<P 𝑦 → ∪ 𝐴
⊊ 𝑦) |
43 | 38, 42 | nsyl 142 |
. 2
⊢ (𝑦 ∈ 𝐴 → ¬ ∪
𝐴<P 𝑦) |
44 | 35, 43 | jctil 523 |
1
⊢ (𝐴 ⊆ P →
((𝑦 ∈ 𝐴 → ¬ ∪ 𝐴<P 𝑦) ∧ (𝑦<P ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑦<P 𝑧))) |