Detailed syntax breakdown of Axiom ax-ac2
Step | Hyp | Ref
| Expression |
1 | | vy |
. . . . . . . 8
setvar 𝑦 |
2 | | vx |
. . . . . . . 8
setvar 𝑥 |
3 | 1, 2 | wel 2112 |
. . . . . . 7
wff 𝑦 ∈ 𝑥 |
4 | | vz |
. . . . . . . . 9
setvar 𝑧 |
5 | 4, 1 | wel 2112 |
. . . . . . . 8
wff 𝑧 ∈ 𝑦 |
6 | | vv |
. . . . . . . . . . 11
setvar 𝑣 |
7 | 6, 2 | wel 2112 |
. . . . . . . . . 10
wff 𝑣 ∈ 𝑥 |
8 | 1, 6 | weq 1971 |
. . . . . . . . . . 11
wff 𝑦 = 𝑣 |
9 | 8 | wn 3 |
. . . . . . . . . 10
wff ¬
𝑦 = 𝑣 |
10 | 7, 9 | wa 399 |
. . . . . . . . 9
wff (𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) |
11 | 4, 6 | wel 2112 |
. . . . . . . . 9
wff 𝑧 ∈ 𝑣 |
12 | 10, 11 | wa 399 |
. . . . . . . 8
wff ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣) |
13 | 5, 12 | wi 4 |
. . . . . . 7
wff (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣)) |
14 | 3, 13 | wa 399 |
. . . . . 6
wff (𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) |
15 | 3 | wn 3 |
. . . . . . 7
wff ¬
𝑦 ∈ 𝑥 |
16 | 4, 2 | wel 2112 |
. . . . . . . 8
wff 𝑧 ∈ 𝑥 |
17 | 6, 4 | wel 2112 |
. . . . . . . . . 10
wff 𝑣 ∈ 𝑧 |
18 | 6, 1 | wel 2112 |
. . . . . . . . . 10
wff 𝑣 ∈ 𝑦 |
19 | 17, 18 | wa 399 |
. . . . . . . . 9
wff (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) |
20 | | vu |
. . . . . . . . . . . 12
setvar 𝑢 |
21 | 20, 4 | wel 2112 |
. . . . . . . . . . 11
wff 𝑢 ∈ 𝑧 |
22 | 20, 1 | wel 2112 |
. . . . . . . . . . 11
wff 𝑢 ∈ 𝑦 |
23 | 21, 22 | wa 399 |
. . . . . . . . . 10
wff (𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) |
24 | 20, 6 | weq 1971 |
. . . . . . . . . 10
wff 𝑢 = 𝑣 |
25 | 23, 24 | wi 4 |
. . . . . . . . 9
wff ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣) |
26 | 19, 25 | wa 399 |
. . . . . . . 8
wff ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)) |
27 | 16, 26 | wi 4 |
. . . . . . 7
wff (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))) |
28 | 15, 27 | wa 399 |
. . . . . 6
wff (¬
𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))) |
29 | 14, 28 | wo 847 |
. . . . 5
wff ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))) |
30 | 29, 20 | wal 1541 |
. . . 4
wff
∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))) |
31 | 30, 6 | wex 1787 |
. . 3
wff
∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))) |
32 | 31, 4 | wal 1541 |
. 2
wff
∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))) |
33 | 32, 1 | wex 1787 |
1
wff
∃𝑦∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))) |