Proof of Theorem bnj1176
Step | Hyp | Ref
| Expression |
1 | | bnj1176.51 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V)) |
2 | | bnj1176.52 |
. . . . . . . . 9
⊢ ((𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V) → ∃𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐶 ¬ 𝑤𝑅𝑧) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐶 ¬ 𝑤𝑅𝑧) |
4 | | df-ral 3066 |
. . . . . . . . 9
⊢
(∀𝑤 ∈
𝐶 ¬ 𝑤𝑅𝑧 ↔ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) |
5 | 4 | rexbii 3170 |
. . . . . . . 8
⊢
(∃𝑧 ∈
𝐶 ∀𝑤 ∈ 𝐶 ¬ 𝑤𝑅𝑧 ↔ ∃𝑧 ∈ 𝐶 ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) |
6 | 3, 5 | sylib 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐶 ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) |
7 | | df-rex 3067 |
. . . . . . 7
⊢
(∃𝑧 ∈
𝐶 ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧) ↔ ∃𝑧(𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) |
8 | 6, 7 | sylib 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ∃𝑧(𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) |
9 | | 19.28v 1999 |
. . . . . . 7
⊢
(∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) ↔ (𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) |
10 | 9 | exbii 1855 |
. . . . . 6
⊢
(∃𝑧∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) ↔ ∃𝑧(𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) |
11 | 8, 10 | sylibr 237 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ∃𝑧∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) |
12 | | 19.37v 2000 |
. . . . 5
⊢
(∃𝑧((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑 ∧ 𝜓) → ∃𝑧∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))) |
13 | 11, 12 | mpbir 234 |
. . . 4
⊢
∃𝑧((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) |
14 | | 19.21v 1947 |
. . . . 5
⊢
(∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))) |
15 | 14 | exbii 1855 |
. . . 4
⊢
(∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ∃𝑧((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))) |
16 | 13, 15 | mpbir 234 |
. . 3
⊢
∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) |
17 | | con2b 363 |
. . . . . . 7
⊢ ((𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧) ↔ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)) |
18 | 17 | anbi2i 626 |
. . . . . 6
⊢ ((𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) ↔ (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))) |
19 | 18 | imbi2i 339 |
. . . . 5
⊢ (((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))) |
20 | 19 | albii 1827 |
. . . 4
⊢
(∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))) |
21 | 20 | exbii 1855 |
. . 3
⊢
(∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))) |
22 | 16, 21 | mpbi 233 |
. 2
⊢
∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))) |
23 | | ax-1 6 |
. . . . 5
⊢ ((𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶) → (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))) |
24 | 23 | anim2i 620 |
. . . 4
⊢ ((𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))) |
25 | 24 | imim2i 16 |
. . 3
⊢ (((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))) → ((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))) |
26 | 25 | alimi 1819 |
. 2
⊢
(∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))) → ∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))) |
27 | 22, 26 | bnj101 32414 |
1
⊢
∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))) |