Proof of Theorem ralcom2
Step | Hyp | Ref
| Expression |
1 | | eleq1 2413 |
. . . . . . 7
⊢ (x = y →
(x ∈
A ↔ y ∈ A)) |
2 | 1 | sps 1754 |
. . . . . 6
⊢ (∀x x = y →
(x ∈
A ↔ y ∈ A)) |
3 | 2 | imbi1d 308 |
. . . . . . . . 9
⊢ (∀x x = y →
((x ∈
A → φ) ↔ (y ∈ A → φ))) |
4 | 3 | dral1 1965 |
. . . . . . . 8
⊢ (∀x x = y →
(∀x(x ∈ A →
φ) ↔ ∀y(y ∈ A → φ))) |
5 | 4 | bicomd 192 |
. . . . . . 7
⊢ (∀x x = y →
(∀y(y ∈ A →
φ) ↔ ∀x(x ∈ A → φ))) |
6 | | df-ral 2619 |
. . . . . . 7
⊢ (∀y ∈ A φ ↔ ∀y(y ∈ A → φ)) |
7 | | df-ral 2619 |
. . . . . . 7
⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ)) |
8 | 5, 6, 7 | 3bitr4g 279 |
. . . . . 6
⊢ (∀x x = y →
(∀y
∈ A φ ↔ ∀x ∈ A φ)) |
9 | 2, 8 | imbi12d 311 |
. . . . 5
⊢ (∀x x = y →
((x ∈
A → ∀y ∈ A φ) ↔ (y ∈ A → ∀x ∈ A φ))) |
10 | 9 | dral1 1965 |
. . . 4
⊢ (∀x x = y →
(∀x(x ∈ A →
∀y
∈ A φ) ↔ ∀y(y ∈ A → ∀x ∈ A φ))) |
11 | | df-ral 2619 |
. . . 4
⊢ (∀x ∈ A ∀y ∈ A φ ↔ ∀x(x ∈ A → ∀y ∈ A φ)) |
12 | | df-ral 2619 |
. . . 4
⊢ (∀y ∈ A ∀x ∈ A φ ↔ ∀y(y ∈ A → ∀x ∈ A φ)) |
13 | 10, 11, 12 | 3bitr4g 279 |
. . 3
⊢ (∀x x = y →
(∀x
∈ A ∀y ∈ A φ ↔ ∀y ∈ A ∀x ∈ A φ)) |
14 | 13 | biimpd 198 |
. 2
⊢ (∀x x = y →
(∀x
∈ A ∀y ∈ A φ → ∀y ∈ A ∀x ∈ A φ)) |
15 | | nfnae 1956 |
. . . . 5
⊢ Ⅎy ¬ ∀x x = y |
16 | | nfra2 2668 |
. . . . 5
⊢ Ⅎy∀x ∈ A ∀y ∈ A φ |
17 | 15, 16 | nfan 1824 |
. . . 4
⊢ Ⅎy(¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) |
18 | | nfnae 1956 |
. . . . . . . 8
⊢ Ⅎx ¬ ∀x x = y |
19 | | nfra1 2664 |
. . . . . . . 8
⊢ Ⅎx∀x ∈ A ∀y ∈ A φ |
20 | 18, 19 | nfan 1824 |
. . . . . . 7
⊢ Ⅎx(¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) |
21 | | nfcvf 2511 |
. . . . . . . . 9
⊢ (¬ ∀x x = y →
Ⅎxy) |
22 | 21 | adantr 451 |
. . . . . . . 8
⊢ ((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) →
Ⅎxy) |
23 | | nfcvd 2490 |
. . . . . . . 8
⊢ ((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) →
ℲxA) |
24 | 22, 23 | nfeld 2504 |
. . . . . . 7
⊢ ((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) →
Ⅎx y ∈ A) |
25 | 20, 24 | nfan1 1881 |
. . . . . 6
⊢ Ⅎx((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) ∧ y ∈ A) |
26 | | rsp2 2676 |
. . . . . . . . 9
⊢ (∀x ∈ A ∀y ∈ A φ → ((x ∈ A ∧ y ∈ A) → φ)) |
27 | 26 | ancomsd 440 |
. . . . . . . 8
⊢ (∀x ∈ A ∀y ∈ A φ → ((y ∈ A ∧ x ∈ A) → φ)) |
28 | 27 | expdimp 426 |
. . . . . . 7
⊢ ((∀x ∈ A ∀y ∈ A φ ∧ y ∈ A) → (x
∈ A
→ φ)) |
29 | 28 | adantll 694 |
. . . . . 6
⊢ (((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) ∧ y ∈ A) →
(x ∈
A → φ)) |
30 | 25, 29 | ralrimi 2695 |
. . . . 5
⊢ (((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) ∧ y ∈ A) →
∀x
∈ A φ) |
31 | 30 | ex 423 |
. . . 4
⊢ ((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) →
(y ∈
A → ∀x ∈ A φ)) |
32 | 17, 31 | ralrimi 2695 |
. . 3
⊢ ((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) →
∀y
∈ A ∀x ∈ A φ) |
33 | 32 | ex 423 |
. 2
⊢ (¬ ∀x x = y →
(∀x
∈ A ∀y ∈ A φ → ∀y ∈ A ∀x ∈ A φ)) |
34 | 14, 33 | pm2.61i 156 |
1
⊢ (∀x ∈ A ∀y ∈ A φ → ∀y ∈ A ∀x ∈ A φ) |