Step | Hyp | Ref
| Expression |
1 | | ralnex 2975 |
. . . . 5
⊢
(∀𝑧 ∈
{𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ [𝑧 / 𝑥]𝜑 ↔ ¬ ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑) |
2 | | vex 3176 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
3 | | sbcng 3443 |
. . . . . . . 8
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑧 / 𝑥]𝜑)) |
4 | 2, 3 | ax-mp 5 |
. . . . . . 7
⊢
([𝑧 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑧 / 𝑥]𝜑) |
5 | 4 | bicomi 213 |
. . . . . 6
⊢ (¬
[𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑥] ¬ 𝜑) |
6 | 5 | ralbii 2963 |
. . . . 5
⊢
(∀𝑧 ∈
{𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥] ¬ 𝜑) |
7 | 1, 6 | bitr3i 265 |
. . . 4
⊢ (¬
∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥] ¬ 𝜑) |
8 | | df-rab 2905 |
. . . . . . 7
⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)} |
9 | 8 | eleq2i 2680 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ↔ 𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)}) |
10 | | df-sbc 3403 |
. . . . . . 7
⊢
([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ 𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)}) |
11 | | sbcan 3445 |
. . . . . . . 8
⊢
([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑)) |
12 | | sbcel1v 3462 |
. . . . . . . . 9
⊢
([𝑧 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) |
13 | 12 | anbi1i 727 |
. . . . . . . 8
⊢
(([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑) ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑)) |
14 | 11, 13 | bitri 263 |
. . . . . . 7
⊢
([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑)) |
15 | 10, 14 | bitr3i 265 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)} ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑)) |
16 | 9, 15 | bitri 263 |
. . . . 5
⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑)) |
17 | 16 | simprbi 479 |
. . . 4
⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → [𝑧 / 𝑥] ¬ 𝜑) |
18 | 7, 17 | mprgbir 2911 |
. . 3
⊢ ¬
∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑 |
19 | | bnj110.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
20 | 19 | rabex 4740 |
. . . . . . . 8
⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V |
21 | 20 | biantrur 526 |
. . . . . . 7
⊢ (𝑅 Fr 𝐴 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V ∧ 𝑅 Fr 𝐴)) |
22 | | rexnal 2978 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑) |
23 | | rabn0 3912 |
. . . . . . . . 9
⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 ¬ 𝜑) |
24 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 |
25 | 24 | biantrur 526 |
. . . . . . . . 9
⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅ ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅)) |
26 | 23, 25 | bitr3i 265 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ¬ 𝜑 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅)) |
27 | 22, 26 | bitr3i 265 |
. . . . . . 7
⊢ (¬
∀𝑥 ∈ 𝐴 𝜑 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅)) |
28 | | fri 5000 |
. . . . . . 7
⊢ ((({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V ∧ 𝑅 Fr 𝐴) ∧ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅)) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧) |
29 | 21, 27, 28 | syl2anb 495 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧) |
30 | | eqid 2610 |
. . . . . . . 8
⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} |
31 | 30 | bnj23 30038 |
. . . . . . 7
⊢
(∀𝑤 ∈
{𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧 → ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)) |
32 | | df-ral 2901 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))) |
33 | 32 | sbcbii 3458 |
. . . . . . . . 9
⊢
([𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ [𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))) |
34 | | sbcal 3452 |
. . . . . . . . . 10
⊢
([𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ∀𝑦[𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))) |
35 | | sbcimg 3444 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))) |
36 | 2, 35 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))) |
37 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
38 | 37 | sbcgf 3468 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
39 | 2, 38 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
([𝑧 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) |
40 | | sbcimg 3444 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑))) |
41 | 2, 40 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑)) |
42 | | sbcbr2g 4640 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅⦋𝑧 / 𝑥⦌𝑥)) |
43 | 2, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅⦋𝑧 / 𝑥⦌𝑥) |
44 | | csbvarg 3955 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ V →
⦋𝑧 / 𝑥⦌𝑥 = 𝑧) |
45 | 2, 44 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
⦋𝑧 /
𝑥⦌𝑥 = 𝑧 |
46 | 45 | breq2i 4591 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦𝑅⦋𝑧 / 𝑥⦌𝑥 ↔ 𝑦𝑅𝑧) |
47 | 43, 46 | bitri 263 |
. . . . . . . . . . . . . . 15
⊢
([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅𝑧) |
48 | | nfsbc1v 3422 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
49 | 48 | sbcgf 3468 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
50 | 2, 49 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
([𝑧 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
51 | 47, 50 | imbi12i 339 |
. . . . . . . . . . . . . 14
⊢
(([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑) ↔ (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)) |
52 | 41, 51 | bitri 263 |
. . . . . . . . . . . . 13
⊢
([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)) |
53 | 39, 52 | imbi12i 339 |
. . . . . . . . . . . 12
⊢
(([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ (𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))) |
54 | 36, 53 | bitri 263 |
. . . . . . . . . . 11
⊢
([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ (𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))) |
55 | 54 | albii 1737 |
. . . . . . . . . 10
⊢
(∀𝑦[𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))) |
56 | 34, 55 | bitri 263 |
. . . . . . . . 9
⊢
([𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))) |
57 | 33, 56 | bitri 263 |
. . . . . . . 8
⊢
([𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))) |
58 | | bnj110.2 |
. . . . . . . . 9
⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) |
59 | 58 | sbcbii 3458 |
. . . . . . . 8
⊢
([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) |
60 | | df-ral 2901 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))) |
61 | 57, 59, 60 | 3bitr4i 291 |
. . . . . . 7
⊢
([𝑧 / 𝑥]𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)) |
62 | 31, 61 | sylibr 223 |
. . . . . 6
⊢
(∀𝑤 ∈
{𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧 → [𝑧 / 𝑥]𝜓) |
63 | 29, 62 | bnj31 30039 |
. . . . 5
⊢ ((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜓) |
64 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑧(𝜓 → 𝜑) |
65 | | nfsbc1v 3422 |
. . . . . . . . 9
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜓 |
66 | | nfsbc1v 3422 |
. . . . . . . . 9
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜑 |
67 | 65, 66 | nfim 1813 |
. . . . . . . 8
⊢
Ⅎ𝑥([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑) |
68 | | sbceq1a 3413 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝜓 ↔ [𝑧 / 𝑥]𝜓)) |
69 | | sbceq1a 3413 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
70 | 68, 69 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → ((𝜓 → 𝜑) ↔ ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑))) |
71 | 64, 67, 70 | cbvral 3143 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝜓 → 𝜑) ↔ ∀𝑧 ∈ 𝐴 ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)) |
72 | | elrabi 3328 |
. . . . . . . . 9
⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → 𝑧 ∈ 𝐴) |
73 | 72 | imim1i 61 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐴 → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)) → (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑))) |
74 | 73 | ralimi2 2933 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝐴 ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑) → ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)) |
75 | 71, 74 | sylbi 206 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 (𝜓 → 𝜑) → ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)) |
76 | | rexim 2991 |
. . . . . 6
⊢
(∀𝑧 ∈
{𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑) → (∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜓 → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑)) |
77 | 75, 76 | syl 17 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝜓 → 𝜑) → (∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜓 → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑)) |
78 | 63, 77 | mpan9 485 |
. . . 4
⊢ (((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑) |
79 | 78 | an32s 842 |
. . 3
⊢ (((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑) |
80 | 18, 79 | mto 187 |
. 2
⊢ ¬
((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) |
81 | | iman 439 |
. 2
⊢ (((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑) ↔ ¬ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑)) |
82 | 80, 81 | mpbir 220 |
1
⊢ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑) |