Detailed syntax breakdown of Axiom ax-ddkcomp
Step | Hyp | Ref
| Expression |
1 | | cA |
. . . . 5
class 𝐴 |
2 | | cr 7760 |
. . . . 5
class
ℝ |
3 | 1, 2 | wss 3121 |
. . . 4
wff 𝐴 ⊆
ℝ |
4 | | vx |
. . . . . . 7
setvar 𝑥 |
5 | 4 | cv 1347 |
. . . . . 6
class 𝑥 |
6 | 5, 1 | wcel 2141 |
. . . . 5
wff 𝑥 ∈ 𝐴 |
7 | 6, 4 | wex 1485 |
. . . 4
wff
∃𝑥 𝑥 ∈ 𝐴 |
8 | 3, 7 | wa 103 |
. . 3
wff (𝐴 ⊆ ℝ ∧
∃𝑥 𝑥 ∈ 𝐴) |
9 | | vy |
. . . . . . 7
setvar 𝑦 |
10 | 9 | cv 1347 |
. . . . . 6
class 𝑦 |
11 | | clt 7941 |
. . . . . 6
class
< |
12 | 10, 5, 11 | wbr 3987 |
. . . . 5
wff 𝑦 < 𝑥 |
13 | 12, 9, 1 | wral 2448 |
. . . 4
wff
∀𝑦 ∈
𝐴 𝑦 < 𝑥 |
14 | 13, 4, 2 | wrex 2449 |
. . 3
wff
∃𝑥 ∈
ℝ ∀𝑦 ∈
𝐴 𝑦 < 𝑥 |
15 | 5, 10, 11 | wbr 3987 |
. . . . . 6
wff 𝑥 < 𝑦 |
16 | | vz |
. . . . . . . . . 10
setvar 𝑧 |
17 | 16 | cv 1347 |
. . . . . . . . 9
class 𝑧 |
18 | 5, 17, 11 | wbr 3987 |
. . . . . . . 8
wff 𝑥 < 𝑧 |
19 | 18, 16, 1 | wrex 2449 |
. . . . . . 7
wff
∃𝑧 ∈
𝐴 𝑥 < 𝑧 |
20 | 17, 10, 11 | wbr 3987 |
. . . . . . . 8
wff 𝑧 < 𝑦 |
21 | 20, 16, 1 | wral 2448 |
. . . . . . 7
wff
∀𝑧 ∈
𝐴 𝑧 < 𝑦 |
22 | 19, 21 | wo 703 |
. . . . . 6
wff
(∃𝑧 ∈
𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦) |
23 | 15, 22 | wi 4 |
. . . . 5
wff (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
24 | 23, 9, 2 | wral 2448 |
. . . 4
wff
∀𝑦 ∈
ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
25 | 24, 4, 2 | wral 2448 |
. . 3
wff
∀𝑥 ∈
ℝ ∀𝑦 ∈
ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
26 | 8, 14, 25 | w3a 973 |
. 2
wff ((𝐴 ⊆ ℝ ∧
∃𝑥 𝑥 ∈ 𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
27 | | cle 7942 |
. . . . . 6
class
≤ |
28 | 10, 5, 27 | wbr 3987 |
. . . . 5
wff 𝑦 ≤ 𝑥 |
29 | 28, 9, 1 | wral 2448 |
. . . 4
wff
∀𝑦 ∈
𝐴 𝑦 ≤ 𝑥 |
30 | | cB |
. . . . . . 7
class 𝐵 |
31 | | cR |
. . . . . . 7
class 𝑅 |
32 | 30, 31 | wcel 2141 |
. . . . . 6
wff 𝐵 ∈ 𝑅 |
33 | 10, 30, 27 | wbr 3987 |
. . . . . . 7
wff 𝑦 ≤ 𝐵 |
34 | 33, 9, 1 | wral 2448 |
. . . . . 6
wff
∀𝑦 ∈
𝐴 𝑦 ≤ 𝐵 |
35 | 32, 34 | wa 103 |
. . . . 5
wff (𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) |
36 | 5, 30, 27 | wbr 3987 |
. . . . 5
wff 𝑥 ≤ 𝐵 |
37 | 35, 36 | wi 4 |
. . . 4
wff ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵) |
38 | 29, 37 | wa 103 |
. . 3
wff
(∀𝑦 ∈
𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵)) |
39 | 38, 4, 2 | wrex 2449 |
. 2
wff
∃𝑥 ∈
ℝ (∀𝑦 ∈
𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵)) |
40 | 26, 39 | wi 4 |
1
wff (((𝐴 ⊆ ℝ ∧
∃𝑥 𝑥 ∈ 𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵))) |