Step | Hyp | Ref
| Expression |
1 | | ralnex 3148 |
. . . . 5
⊢
(∀𝑧 ∈
{𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ [𝑧 / 𝑥]𝜑 ↔ ¬ ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑) |
2 | | sbcng 3726 |
. . . . . . . 8
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑧 / 𝑥]𝜑)) |
3 | 2 | elv 3403 |
. . . . . . 7
⊢
([𝑧 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑧 / 𝑥]𝜑) |
4 | 3 | bicomi 227 |
. . . . . 6
⊢ (¬
[𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑥] ¬ 𝜑) |
5 | 4 | ralbii 3080 |
. . . . 5
⊢
(∀𝑧 ∈
{𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥] ¬ 𝜑) |
6 | 1, 5 | bitr3i 280 |
. . . 4
⊢ (¬
∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥] ¬ 𝜑) |
7 | | df-rab 3062 |
. . . . . . 7
⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)} |
8 | 7 | eleq2i 2824 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ↔ 𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)}) |
9 | | df-sbc 3680 |
. . . . . . 7
⊢
([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ 𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)}) |
10 | | sbcan 3728 |
. . . . . . . 8
⊢
([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑)) |
11 | | sbcel1v 3746 |
. . . . . . . . 9
⊢
([𝑧 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) |
12 | 11 | anbi1i 627 |
. . . . . . . 8
⊢
(([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑) ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑)) |
13 | 10, 12 | bitri 278 |
. . . . . . 7
⊢
([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑)) |
14 | 9, 13 | bitr3i 280 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)} ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑)) |
15 | 8, 14 | bitri 278 |
. . . . 5
⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑)) |
16 | 15 | simprbi 500 |
. . . 4
⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → [𝑧 / 𝑥] ¬ 𝜑) |
17 | 6, 16 | mprgbir 3068 |
. . 3
⊢ ¬
∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑 |
18 | | bnj110.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
19 | 18 | rabex 5197 |
. . . . . . . 8
⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V |
20 | 19 | biantrur 534 |
. . . . . . 7
⊢ (𝑅 Fr 𝐴 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V ∧ 𝑅 Fr 𝐴)) |
21 | | rexnal 3150 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑) |
22 | | rabn0 4271 |
. . . . . . . . 9
⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 ¬ 𝜑) |
23 | | ssrab2 3967 |
. . . . . . . . . 10
⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 |
24 | 23 | biantrur 534 |
. . . . . . . . 9
⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅ ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅)) |
25 | 22, 24 | bitr3i 280 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ¬ 𝜑 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅)) |
26 | 21, 25 | bitr3i 280 |
. . . . . . 7
⊢ (¬
∀𝑥 ∈ 𝐴 𝜑 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅)) |
27 | | fri 5481 |
. . . . . . 7
⊢ ((({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V ∧ 𝑅 Fr 𝐴) ∧ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅)) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧) |
28 | 20, 26, 27 | syl2anb 601 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧) |
29 | | eqid 2738 |
. . . . . . . 8
⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} |
30 | 29 | bnj23 32259 |
. . . . . . 7
⊢
(∀𝑤 ∈
{𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧 → ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)) |
31 | | df-ral 3058 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))) |
32 | 31 | sbcbii 3736 |
. . . . . . . . 9
⊢
([𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ [𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))) |
33 | | sbcal 3740 |
. . . . . . . . . 10
⊢
([𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ∀𝑦[𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))) |
34 | | sbcimg 3727 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))) |
35 | 34 | elv 3403 |
. . . . . . . . . . . 12
⊢
([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))) |
36 | | vex 3401 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
37 | | nfv 1920 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
38 | 36, 37 | sbcgfi 3754 |
. . . . . . . . . . . . 13
⊢
([𝑧 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) |
39 | | sbcimg 3727 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑))) |
40 | 39 | elv 3403 |
. . . . . . . . . . . . . 14
⊢
([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑)) |
41 | | sbcbr2g 5085 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅⦋𝑧 / 𝑥⦌𝑥)) |
42 | 41 | elv 3403 |
. . . . . . . . . . . . . . . 16
⊢
([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅⦋𝑧 / 𝑥⦌𝑥) |
43 | 36 | csbvargi 4319 |
. . . . . . . . . . . . . . . . 17
⊢
⦋𝑧 /
𝑥⦌𝑥 = 𝑧 |
44 | 43 | breq2i 5035 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦𝑅⦋𝑧 / 𝑥⦌𝑥 ↔ 𝑦𝑅𝑧) |
45 | 42, 44 | bitri 278 |
. . . . . . . . . . . . . . 15
⊢
([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅𝑧) |
46 | | nfsbc1v 3699 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
47 | 36, 46 | sbcgfi 3754 |
. . . . . . . . . . . . . . 15
⊢
([𝑧 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
48 | 45, 47 | imbi12i 354 |
. . . . . . . . . . . . . 14
⊢
(([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑) ↔ (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)) |
49 | 40, 48 | bitri 278 |
. . . . . . . . . . . . 13
⊢
([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)) |
50 | 38, 49 | imbi12i 354 |
. . . . . . . . . . . 12
⊢
(([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ (𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))) |
51 | 35, 50 | bitri 278 |
. . . . . . . . . . 11
⊢
([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ (𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))) |
52 | 51 | albii 1826 |
. . . . . . . . . 10
⊢
(∀𝑦[𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))) |
53 | 33, 52 | bitri 278 |
. . . . . . . . 9
⊢
([𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))) |
54 | 32, 53 | bitri 278 |
. . . . . . . 8
⊢
([𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))) |
55 | | bnj110.2 |
. . . . . . . . 9
⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) |
56 | 55 | sbcbii 3736 |
. . . . . . . 8
⊢
([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) |
57 | | df-ral 3058 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))) |
58 | 54, 56, 57 | 3bitr4i 306 |
. . . . . . 7
⊢
([𝑧 / 𝑥]𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)) |
59 | 30, 58 | sylibr 237 |
. . . . . 6
⊢
(∀𝑤 ∈
{𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧 → [𝑧 / 𝑥]𝜓) |
60 | 28, 59 | bnj31 32260 |
. . . . 5
⊢ ((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜓) |
61 | | nfv 1920 |
. . . . . . . 8
⊢
Ⅎ𝑧(𝜓 → 𝜑) |
62 | | nfsbc1v 3699 |
. . . . . . . . 9
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜓 |
63 | | nfsbc1v 3699 |
. . . . . . . . 9
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜑 |
64 | 62, 63 | nfim 1902 |
. . . . . . . 8
⊢
Ⅎ𝑥([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑) |
65 | | sbceq1a 3690 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝜓 ↔ [𝑧 / 𝑥]𝜓)) |
66 | | sbceq1a 3690 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
67 | 65, 66 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → ((𝜓 → 𝜑) ↔ ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑))) |
68 | 61, 64, 67 | cbvralw 3339 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝜓 → 𝜑) ↔ ∀𝑧 ∈ 𝐴 ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)) |
69 | | elrabi 3579 |
. . . . . . . . 9
⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → 𝑧 ∈ 𝐴) |
70 | 69 | imim1i 63 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐴 → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)) → (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑))) |
71 | 70 | ralimi2 3072 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝐴 ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑) → ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)) |
72 | 68, 71 | sylbi 220 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 (𝜓 → 𝜑) → ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)) |
73 | | rexim 3153 |
. . . . . 6
⊢
(∀𝑧 ∈
{𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑) → (∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜓 → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑)) |
74 | 72, 73 | syl 17 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝜓 → 𝜑) → (∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜓 → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑)) |
75 | 60, 74 | mpan9 510 |
. . . 4
⊢ (((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑) |
76 | 75 | an32s 652 |
. . 3
⊢ (((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑) |
77 | 17, 76 | mto 200 |
. 2
⊢ ¬
((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) |
78 | | iman 405 |
. 2
⊢ (((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑) ↔ ¬ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑)) |
79 | 77, 78 | mpbir 234 |
1
⊢ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑) |