Proof of Theorem 2ralor
Step | Hyp | Ref
| Expression |
1 | | rexnal 2625 |
. . . 4
⊢ (∃x ∈ A ¬ φ ↔ ¬ ∀x ∈ A φ) |
2 | | rexnal 2625 |
. . . 4
⊢ (∃y ∈ B ¬ ψ ↔ ¬ ∀y ∈ B ψ) |
3 | 1, 2 | anbi12i 678 |
. . 3
⊢ ((∃x ∈ A ¬ φ ∧ ∃y ∈ B ¬ ψ) ↔ (¬ ∀x ∈ A φ ∧ ¬
∀y
∈ B ψ)) |
4 | | ioran 476 |
. . . . . . 7
⊢ (¬ (φ ∨ ψ) ↔ (¬ φ ∧ ¬
ψ)) |
5 | 4 | rexbii 2639 |
. . . . . 6
⊢ (∃y ∈ B ¬
(φ ∨
ψ) ↔ ∃y ∈ B (¬
φ ∧
¬ ψ)) |
6 | | rexnal 2625 |
. . . . . 6
⊢ (∃y ∈ B ¬
(φ ∨
ψ) ↔ ¬ ∀y ∈ B (φ ∨ ψ)) |
7 | 5, 6 | bitr3i 242 |
. . . . 5
⊢ (∃y ∈ B (¬
φ ∧
¬ ψ) ↔ ¬ ∀y ∈ B (φ ∨ ψ)) |
8 | 7 | rexbii 2639 |
. . . 4
⊢ (∃x ∈ A ∃y ∈ B (¬
φ ∧
¬ ψ) ↔ ∃x ∈ A ¬ ∀y ∈ B (φ ∨ ψ)) |
9 | | reeanv 2778 |
. . . 4
⊢ (∃x ∈ A ∃y ∈ B (¬
φ ∧
¬ ψ) ↔ (∃x ∈ A ¬ φ ∧ ∃y ∈ B ¬ ψ)) |
10 | | rexnal 2625 |
. . . 4
⊢ (∃x ∈ A ¬ ∀y ∈ B (φ ∨ ψ) ↔ ¬ ∀x ∈ A ∀y ∈ B (φ ∨ ψ)) |
11 | 8, 9, 10 | 3bitr3ri 267 |
. . 3
⊢ (¬ ∀x ∈ A ∀y ∈ B (φ ∨ ψ) ↔ (∃x ∈ A ¬ φ ∧ ∃y ∈ B ¬ ψ)) |
12 | | ioran 476 |
. . 3
⊢ (¬ (∀x ∈ A φ ∨ ∀y ∈ B ψ) ↔ (¬ ∀x ∈ A φ ∧ ¬
∀y
∈ B ψ)) |
13 | 3, 11, 12 | 3bitr4i 268 |
. 2
⊢ (¬ ∀x ∈ A ∀y ∈ B (φ ∨ ψ) ↔ ¬ (∀x ∈ A φ ∨ ∀y ∈ B ψ)) |
14 | 13 | con4bii 288 |
1
⊢ (∀x ∈ A ∀y ∈ B (φ ∨ ψ) ↔ (∀x ∈ A φ ∨ ∀y ∈ B ψ)) |