Proof of Theorem 2reu5lem3
Step | Hyp | Ref
| Expression |
1 | | 2reu5lem1 3041 |
. . 3
⊢ (∃!x ∈ A ∃!y ∈ B φ ↔ ∃!x∃!y(x ∈ A ∧ y ∈ B ∧ φ)) |
2 | | 2reu5lem2 3042 |
. . 3
⊢ (∀x ∈ A ∃*y ∈ B φ ↔ ∀x∃*y(x ∈ A ∧ y ∈ B ∧ φ)) |
3 | 1, 2 | anbi12i 678 |
. 2
⊢ ((∃!x ∈ A ∃!y ∈ B φ ∧ ∀x ∈ A ∃*y ∈ B φ) ↔ (∃!x∃!y(x ∈ A ∧ y ∈ B ∧ φ) ∧ ∀x∃*y(x ∈ A ∧ y ∈ B ∧ φ))) |
4 | | 2eu5 2288 |
. 2
⊢ ((∃!x∃!y(x ∈ A ∧ y ∈ B ∧ φ) ∧ ∀x∃*y(x ∈ A ∧ y ∈ B ∧ φ)) ↔ (∃x∃y(x ∈ A ∧ y ∈ B ∧ φ) ∧ ∃z∃w∀x∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)))) |
5 | | 3anass 938 |
. . . . . . 7
⊢ ((x ∈ A ∧ y ∈ B ∧ φ) ↔ (x ∈ A ∧ (y ∈ B ∧ φ))) |
6 | 5 | exbii 1582 |
. . . . . 6
⊢ (∃y(x ∈ A ∧ y ∈ B ∧ φ) ↔ ∃y(x ∈ A ∧ (y ∈ B ∧ φ))) |
7 | | 19.42v 1905 |
. . . . . 6
⊢ (∃y(x ∈ A ∧ (y ∈ B ∧ φ)) ↔ (x ∈ A ∧ ∃y(y ∈ B ∧ φ))) |
8 | | df-rex 2620 |
. . . . . . . 8
⊢ (∃y ∈ B φ ↔ ∃y(y ∈ B ∧ φ)) |
9 | 8 | bicomi 193 |
. . . . . . 7
⊢ (∃y(y ∈ B ∧ φ) ↔ ∃y ∈ B φ) |
10 | 9 | anbi2i 675 |
. . . . . 6
⊢ ((x ∈ A ∧ ∃y(y ∈ B ∧ φ)) ↔ (x ∈ A ∧ ∃y ∈ B φ)) |
11 | 6, 7, 10 | 3bitri 262 |
. . . . 5
⊢ (∃y(x ∈ A ∧ y ∈ B ∧ φ) ↔ (x ∈ A ∧ ∃y ∈ B φ)) |
12 | 11 | exbii 1582 |
. . . 4
⊢ (∃x∃y(x ∈ A ∧ y ∈ B ∧ φ) ↔ ∃x(x ∈ A ∧ ∃y ∈ B φ)) |
13 | | df-rex 2620 |
. . . 4
⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x(x ∈ A ∧ ∃y ∈ B φ)) |
14 | 12, 13 | bitr4i 243 |
. . 3
⊢ (∃x∃y(x ∈ A ∧ y ∈ B ∧ φ) ↔ ∃x ∈ A ∃y ∈ B φ) |
15 | | 3anan12 947 |
. . . . . . . . . . 11
⊢ ((x ∈ A ∧ y ∈ B ∧ φ) ↔ (y ∈ B ∧ (x ∈ A ∧ φ))) |
16 | 15 | imbi1i 315 |
. . . . . . . . . 10
⊢ (((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ ((y
∈ B ∧ (x ∈ A ∧ φ)) →
(x = z
∧ y =
w))) |
17 | | impexp 433 |
. . . . . . . . . 10
⊢ (((y ∈ B ∧ (x ∈ A ∧ φ)) → (x = z ∧ y = w)) ↔ (y
∈ B
→ ((x ∈ A ∧ φ) →
(x = z
∧ y =
w)))) |
18 | | impexp 433 |
. . . . . . . . . . 11
⊢ (((x ∈ A ∧ φ) → (x = z ∧ y = w)) ↔ (x
∈ A
→ (φ → (x = z ∧ y = w)))) |
19 | 18 | imbi2i 303 |
. . . . . . . . . 10
⊢ ((y ∈ B → ((x
∈ A ∧ φ) →
(x = z
∧ y =
w))) ↔ (y ∈ B → (x
∈ A
→ (φ → (x = z ∧ y = w))))) |
20 | 16, 17, 19 | 3bitri 262 |
. . . . . . . . 9
⊢ (((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ (y
∈ B
→ (x ∈ A →
(φ → (x = z ∧ y = w))))) |
21 | 20 | albii 1566 |
. . . . . . . 8
⊢ (∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ ∀y(y ∈ B → (x
∈ A
→ (φ → (x = z ∧ y = w))))) |
22 | | df-ral 2619 |
. . . . . . . 8
⊢ (∀y ∈ B (x ∈ A → (φ
→ (x = z ∧ y = w))) ↔
∀y(y ∈ B →
(x ∈
A → (φ → (x = z ∧ y = w))))) |
23 | | r19.21v 2701 |
. . . . . . . 8
⊢ (∀y ∈ B (x ∈ A → (φ
→ (x = z ∧ y = w))) ↔
(x ∈
A → ∀y ∈ B (φ → (x = z ∧ y = w)))) |
24 | 21, 22, 23 | 3bitr2i 264 |
. . . . . . 7
⊢ (∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ (x
∈ A
→ ∀y ∈ B (φ →
(x = z
∧ y =
w)))) |
25 | 24 | albii 1566 |
. . . . . 6
⊢ (∀x∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ ∀x(x ∈ A → ∀y ∈ B (φ → (x = z ∧ y = w)))) |
26 | | df-ral 2619 |
. . . . . 6
⊢ (∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)) ↔ ∀x(x ∈ A → ∀y ∈ B (φ → (x = z ∧ y = w)))) |
27 | 25, 26 | bitr4i 243 |
. . . . 5
⊢ (∀x∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))) |
28 | 27 | exbii 1582 |
. . . 4
⊢ (∃w∀x∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ ∃w∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))) |
29 | 28 | exbii 1582 |
. . 3
⊢ (∃z∃w∀x∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ ∃z∃w∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))) |
30 | 14, 29 | anbi12i 678 |
. 2
⊢ ((∃x∃y(x ∈ A ∧ y ∈ B ∧ φ) ∧ ∃z∃w∀x∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w))) ↔ (∃x ∈ A ∃y ∈ B φ ∧ ∃z∃w∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)))) |
31 | 3, 4, 30 | 3bitri 262 |
1
⊢ ((∃!x ∈ A ∃!y ∈ B φ ∧ ∀x ∈ A ∃*y ∈ B φ) ↔ (∃x ∈ A ∃y ∈ B φ ∧ ∃z∃w∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)))) |