Proof of Theorem bnj1388
Step | Hyp | Ref
| Expression |
1 | | bnj1388.7 |
. . 3
⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) |
2 | | nfv 1921 |
. . . 4
⊢
Ⅎ𝑦𝜓 |
3 | | nfv 1921 |
. . . 4
⊢
Ⅎ𝑦 𝑥 ∈ 𝐷 |
4 | | nfra1 3145 |
. . . 4
⊢
Ⅎ𝑦∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥 |
5 | 2, 3, 4 | nf3an 1908 |
. . 3
⊢
Ⅎ𝑦(𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥) |
6 | 1, 5 | nfxfr 1859 |
. 2
⊢
Ⅎ𝑦𝜒 |
7 | | bnj1152 32987 |
. . . . . 6
⊢ (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑥)) |
8 | 7 | simplbi 498 |
. . . . 5
⊢ (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → 𝑦 ∈ 𝐴) |
9 | 8 | adantl 482 |
. . . 4
⊢ ((𝜒 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) → 𝑦 ∈ 𝐴) |
10 | 7 | biimpi 215 |
. . . . . . . . 9
⊢ (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑥)) |
11 | 10 | adantl 482 |
. . . . . . . 8
⊢ ((𝜒 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) → (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑥)) |
12 | 11 | simprd 496 |
. . . . . . 7
⊢ ((𝜒 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) → 𝑦𝑅𝑥) |
13 | 1 | simp3bi 1146 |
. . . . . . . 8
⊢ (𝜒 → ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ ((𝜒 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) → ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥) |
15 | | df-ral 3071 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝐷 ¬ 𝑦𝑅𝑥 ↔ ∀𝑦(𝑦 ∈ 𝐷 → ¬ 𝑦𝑅𝑥)) |
16 | | con2b 360 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐷 → ¬ 𝑦𝑅𝑥) ↔ (𝑦𝑅𝑥 → ¬ 𝑦 ∈ 𝐷)) |
17 | 16 | albii 1826 |
. . . . . . . . 9
⊢
(∀𝑦(𝑦 ∈ 𝐷 → ¬ 𝑦𝑅𝑥) ↔ ∀𝑦(𝑦𝑅𝑥 → ¬ 𝑦 ∈ 𝐷)) |
18 | 15, 17 | bitri 274 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝐷 ¬ 𝑦𝑅𝑥 ↔ ∀𝑦(𝑦𝑅𝑥 → ¬ 𝑦 ∈ 𝐷)) |
19 | | sp 2180 |
. . . . . . . . 9
⊢
(∀𝑦(𝑦𝑅𝑥 → ¬ 𝑦 ∈ 𝐷) → (𝑦𝑅𝑥 → ¬ 𝑦 ∈ 𝐷)) |
20 | 19 | impcom 408 |
. . . . . . . 8
⊢ ((𝑦𝑅𝑥 ∧ ∀𝑦(𝑦𝑅𝑥 → ¬ 𝑦 ∈ 𝐷)) → ¬ 𝑦 ∈ 𝐷) |
21 | 18, 20 | sylan2b 594 |
. . . . . . 7
⊢ ((𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥) → ¬ 𝑦 ∈ 𝐷) |
22 | 12, 14, 21 | syl2anc 584 |
. . . . . 6
⊢ ((𝜒 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) → ¬ 𝑦 ∈ 𝐷) |
23 | | bnj1388.5 |
. . . . . . . 8
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} |
24 | 23 | eleq2i 2832 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐷 ↔ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}) |
25 | | nfcv 2909 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑦 |
26 | | nfcv 2909 |
. . . . . . . 8
⊢
Ⅎ𝑥𝐴 |
27 | | bnj1388.8 |
. . . . . . . . . . 11
⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) |
28 | | nfsbc1v 3740 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜏 |
29 | 27, 28 | nfxfr 1859 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝜏′ |
30 | 29 | nfex 2322 |
. . . . . . . . 9
⊢
Ⅎ𝑥∃𝑓𝜏′ |
31 | 30 | nfn 1864 |
. . . . . . . 8
⊢
Ⅎ𝑥 ¬
∃𝑓𝜏′ |
32 | | sbceq1a 3731 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝜏 ↔ [𝑦 / 𝑥]𝜏)) |
33 | 32, 27 | bitr4di 289 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝜏 ↔ 𝜏′)) |
34 | 33 | exbidv 1928 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (∃𝑓𝜏 ↔ ∃𝑓𝜏′)) |
35 | 34 | notbid 318 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (¬ ∃𝑓𝜏 ↔ ¬ ∃𝑓𝜏′)) |
36 | 25, 26, 31, 35 | elrabf 3622 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} ↔ (𝑦 ∈ 𝐴 ∧ ¬ ∃𝑓𝜏′)) |
37 | 24, 36 | bitri 274 |
. . . . . 6
⊢ (𝑦 ∈ 𝐷 ↔ (𝑦 ∈ 𝐴 ∧ ¬ ∃𝑓𝜏′)) |
38 | 22, 37 | sylnib 328 |
. . . . 5
⊢ ((𝜒 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) → ¬ (𝑦 ∈ 𝐴 ∧ ¬ ∃𝑓𝜏′)) |
39 | | iman 402 |
. . . . 5
⊢ ((𝑦 ∈ 𝐴 → ∃𝑓𝜏′) ↔ ¬ (𝑦 ∈ 𝐴 ∧ ¬ ∃𝑓𝜏′)) |
40 | 38, 39 | sylibr 233 |
. . . 4
⊢ ((𝜒 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) → (𝑦 ∈ 𝐴 → ∃𝑓𝜏′)) |
41 | 9, 40 | mpd 15 |
. . 3
⊢ ((𝜒 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) → ∃𝑓𝜏′) |
42 | 41 | ex 413 |
. 2
⊢ (𝜒 → (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → ∃𝑓𝜏′)) |
43 | 6, 42 | ralrimi 3142 |
1
⊢ (𝜒 → ∀𝑦 ∈ pred (𝑥, 𝐴, 𝑅)∃𝑓𝜏′) |