Proof of Theorem bj-xnex
Step | Hyp | Ref
| Expression |
1 | | nfa1 2015 |
. . . . 5
⊢
Ⅎ𝑦∀𝑦(𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) |
2 | | nfe1 2014 |
. . . . . . 7
⊢
Ⅎ𝑦∃𝑦 𝑥 = 𝐴 |
3 | 2 | nfab 2755 |
. . . . . 6
⊢
Ⅎ𝑦{𝑥 ∣ ∃𝑦 𝑥 = 𝐴} |
4 | 3 | nfuni 4378 |
. . . . 5
⊢
Ⅎ𝑦∪ {𝑥
∣ ∃𝑦 𝑥 = 𝐴} |
5 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑦V |
6 | | vex 3176 |
. . . . . . 7
⊢ 𝑦 ∈ V |
7 | 6 | 2a1i 12 |
. . . . . 6
⊢
(∀𝑦(𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ ∪ {𝑥 ∣ ∃𝑦 𝑥 = 𝐴} → 𝑦 ∈ V)) |
8 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐴 |
9 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
10 | | eleq2 2677 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴)) |
11 | 10 | biimprd 237 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝑥)) |
12 | | 19.8a 2039 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → ∃𝑦 𝑥 = 𝐴) |
13 | 11, 12 | jctird 565 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝐴 → (𝑦 ∈ 𝑥 ∧ ∃𝑦 𝑥 = 𝐴))) |
14 | 8, 9, 13 | spcimegf 3260 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝑦 ∈ 𝐴 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∃𝑦 𝑥 = 𝐴))) |
15 | 14 | imp 444 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∃𝑦 𝑥 = 𝐴)) |
16 | 15 | sps 2043 |
. . . . . . . 8
⊢
(∀𝑦(𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∃𝑦 𝑥 = 𝐴)) |
17 | | eluniab 4383 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ {𝑥
∣ ∃𝑦 𝑥 = 𝐴} ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∃𝑦 𝑥 = 𝐴)) |
18 | 16, 17 | sylibr 223 |
. . . . . . 7
⊢
(∀𝑦(𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ∪ {𝑥 ∣ ∃𝑦 𝑥 = 𝐴}) |
19 | 18 | a1d 25 |
. . . . . 6
⊢
(∀𝑦(𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ V → 𝑦 ∈ ∪ {𝑥 ∣ ∃𝑦 𝑥 = 𝐴})) |
20 | 7, 19 | impbid 201 |
. . . . 5
⊢
(∀𝑦(𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ ∪ {𝑥 ∣ ∃𝑦 𝑥 = 𝐴} ↔ 𝑦 ∈ V)) |
21 | 1, 4, 5, 20 | eqrd 3586 |
. . . 4
⊢
(∀𝑦(𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ∪ {𝑥 ∣ ∃𝑦 𝑥 = 𝐴} = V) |
22 | | vprc 4724 |
. . . . 5
⊢ ¬ V
∈ V |
23 | 22 | a1i 11 |
. . . 4
⊢
(∀𝑦(𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ¬ V ∈ V) |
24 | 21, 23 | eqneltrd 2707 |
. . 3
⊢
(∀𝑦(𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ¬ ∪
{𝑥 ∣ ∃𝑦 𝑥 = 𝐴} ∈ V) |
25 | | uniexg 6853 |
. . 3
⊢ ({𝑥 ∣ ∃𝑦 𝑥 = 𝐴} ∈ V → ∪ {𝑥
∣ ∃𝑦 𝑥 = 𝐴} ∈ V) |
26 | 24, 25 | nsyl 134 |
. 2
⊢
(∀𝑦(𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ¬ {𝑥 ∣ ∃𝑦 𝑥 = 𝐴} ∈ V) |
27 | | df-nel 2783 |
. 2
⊢ ({𝑥 ∣ ∃𝑦 𝑥 = 𝐴} ∉ V ↔ ¬ {𝑥 ∣ ∃𝑦 𝑥 = 𝐴} ∈ V) |
28 | 26, 27 | sylibr 223 |
1
⊢
(∀𝑦(𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → {𝑥 ∣ ∃𝑦 𝑥 = 𝐴} ∉ V) |