Step |
Hyp |
Ref |
Expression |
1 |
|
df-id |
⊢ I = { 〈 𝑥 , 𝑧 〉 ∣ 𝑥 = 𝑧 } |
2 |
|
equcom |
⊢ ( 𝑥 = 𝑧 ↔ 𝑧 = 𝑥 ) |
3 |
2
|
anbi1ci |
⊢ ( ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) ↔ ( 𝑧 = 𝑥 ∧ 𝑤 = 〈 𝑥 , 𝑧 〉 ) ) |
4 |
3
|
exbii |
⊢ ( ∃ 𝑧 ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑤 = 〈 𝑥 , 𝑧 〉 ) ) |
5 |
|
opeq2 |
⊢ ( 𝑧 = 𝑥 → 〈 𝑥 , 𝑧 〉 = 〈 𝑥 , 𝑥 〉 ) |
6 |
5
|
eqeq2d |
⊢ ( 𝑧 = 𝑥 → ( 𝑤 = 〈 𝑥 , 𝑧 〉 ↔ 𝑤 = 〈 𝑥 , 𝑥 〉 ) ) |
7 |
6
|
equsexvw |
⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑤 = 〈 𝑥 , 𝑧 〉 ) ↔ 𝑤 = 〈 𝑥 , 𝑥 〉 ) |
8 |
|
equid |
⊢ 𝑥 = 𝑥 |
9 |
8
|
biantru |
⊢ ( 𝑤 = 〈 𝑥 , 𝑥 〉 ↔ ( 𝑤 = 〈 𝑥 , 𝑥 〉 ∧ 𝑥 = 𝑥 ) ) |
10 |
4 7 9
|
3bitri |
⊢ ( ∃ 𝑧 ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) ↔ ( 𝑤 = 〈 𝑥 , 𝑥 〉 ∧ 𝑥 = 𝑥 ) ) |
11 |
10
|
exbii |
⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ( 𝑤 = 〈 𝑥 , 𝑥 〉 ∧ 𝑥 = 𝑥 ) ) |
12 |
|
nfe1 |
⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑤 = 〈 𝑥 , 𝑥 〉 ∧ 𝑥 = 𝑥 ) |
13 |
12
|
19.9 |
⊢ ( ∃ 𝑥 ∃ 𝑥 ( 𝑤 = 〈 𝑥 , 𝑥 〉 ∧ 𝑥 = 𝑥 ) ↔ ∃ 𝑥 ( 𝑤 = 〈 𝑥 , 𝑥 〉 ∧ 𝑥 = 𝑥 ) ) |
14 |
11 13
|
bitr4i |
⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑥 ( 𝑤 = 〈 𝑥 , 𝑥 〉 ∧ 𝑥 = 𝑥 ) ) |
15 |
|
opeq2 |
⊢ ( 𝑥 = 𝑦 → 〈 𝑥 , 𝑥 〉 = 〈 𝑥 , 𝑦 〉 ) |
16 |
15
|
eqeq2d |
⊢ ( 𝑥 = 𝑦 → ( 𝑤 = 〈 𝑥 , 𝑥 〉 ↔ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ) |
17 |
|
equequ2 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑥 ↔ 𝑥 = 𝑦 ) ) |
18 |
16 17
|
anbi12d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑤 = 〈 𝑥 , 𝑥 〉 ∧ 𝑥 = 𝑥 ) ↔ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 = 𝑦 ) ) ) |
19 |
18
|
sps |
⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑤 = 〈 𝑥 , 𝑥 〉 ∧ 𝑥 = 𝑥 ) ↔ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 = 𝑦 ) ) ) |
20 |
19
|
drex1 |
⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ( 𝑤 = 〈 𝑥 , 𝑥 〉 ∧ 𝑥 = 𝑥 ) ↔ ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 = 𝑦 ) ) ) |
21 |
20
|
drex2 |
⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∃ 𝑥 ( 𝑤 = 〈 𝑥 , 𝑥 〉 ∧ 𝑥 = 𝑥 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 = 𝑦 ) ) ) |
22 |
14 21
|
syl5bb |
⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 = 𝑦 ) ) ) |
23 |
|
nfnae |
⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 |
24 |
|
nfnae |
⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 |
25 |
|
nfcvd |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑤 ) |
26 |
|
nfcvf2 |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 ) |
27 |
|
nfcvd |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑧 ) |
28 |
26 27
|
nfopd |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 〈 𝑥 , 𝑧 〉 ) |
29 |
25 28
|
nfeqd |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑤 = 〈 𝑥 , 𝑧 〉 ) |
30 |
26 27
|
nfeqd |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 = 𝑧 ) |
31 |
29 30
|
nfand |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) ) |
32 |
|
opeq2 |
⊢ ( 𝑧 = 𝑦 → 〈 𝑥 , 𝑧 〉 = 〈 𝑥 , 𝑦 〉 ) |
33 |
32
|
eqeq2d |
⊢ ( 𝑧 = 𝑦 → ( 𝑤 = 〈 𝑥 , 𝑧 〉 ↔ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ) |
34 |
|
equequ2 |
⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑥 = 𝑦 ) ) |
35 |
33 34
|
anbi12d |
⊢ ( 𝑧 = 𝑦 → ( ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) ↔ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 = 𝑦 ) ) ) |
36 |
35
|
a1i |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ( ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) ↔ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 = 𝑦 ) ) ) ) |
37 |
24 31 36
|
cbvexd |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑧 ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 = 𝑦 ) ) ) |
38 |
23 37
|
exbid |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 = 𝑦 ) ) ) |
39 |
22 38
|
pm2.61i |
⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 = 𝑦 ) ) |
40 |
39
|
abbii |
⊢ { 𝑤 ∣ ∃ 𝑥 ∃ 𝑧 ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 = 𝑦 ) } |
41 |
|
df-opab |
⊢ { 〈 𝑥 , 𝑧 〉 ∣ 𝑥 = 𝑧 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑧 ( 𝑤 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 = 𝑧 ) } |
42 |
|
df-opab |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 = 𝑦 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 = 𝑦 ) } |
43 |
40 41 42
|
3eqtr4i |
⊢ { 〈 𝑥 , 𝑧 〉 ∣ 𝑥 = 𝑧 } = { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 = 𝑦 } |
44 |
1 43
|
eqtri |
⊢ I = { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 = 𝑦 } |