Step | Hyp | Ref
| Expression |
1 | | oveq12 5464 |
. . . . . 6
⊢
((z = A ∧ u = 𝐷) → (z ·𝑜 u) = (A
·𝑜 𝐷)) |
2 | | oveq12 5464 |
. . . . . 6
⊢
((w = B ∧ v = 𝐶) → (w ·𝑜 v) = (B
·𝑜 𝐶)) |
3 | 1, 2 | eqeqan12d 2052 |
. . . . 5
⊢
(((z = A ∧ u = 𝐷) ∧
(w = B
∧ v =
𝐶)) → ((z ·𝑜 u) = (w
·𝑜 v) ↔
(A ·𝑜 𝐷) = (B ·𝑜 𝐶))) |
4 | 3 | an42s 523 |
. . . 4
⊢
(((z = A ∧ w = B) ∧ (v = 𝐶 ∧ u = 𝐷)) → ((z ·𝑜 u) = (w
·𝑜 v) ↔
(A ·𝑜 𝐷) = (B ·𝑜 𝐶))) |
5 | 4 | copsex4g 3975 |
. . 3
⊢
(((A ∈ 𝜔 ∧
B ∈
N) ∧ (𝐶 ∈
𝜔 ∧ 𝐷 ∈
N)) → (∃z∃w∃v∃u((〈A,
B〉 = 〈z, w〉 ∧ 〈𝐶, 𝐷〉 = 〈v, u〉)
∧ (z
·𝑜 u) = (w ·𝑜 v)) ↔ (A
·𝑜 𝐷) = (B
·𝑜 𝐶))) |
6 | 5 | anbi2d 437 |
. 2
⊢
(((A ∈ 𝜔 ∧
B ∈
N) ∧ (𝐶 ∈
𝜔 ∧ 𝐷 ∈
N)) → (((〈A,
B〉 ∈
(𝜔 × N) ∧
〈𝐶, 𝐷〉 ∈
(𝜔 × N)) ∧ ∃z∃w∃v∃u((〈A,
B〉 = 〈z, w〉 ∧ 〈𝐶, 𝐷〉 = 〈v, u〉)
∧ (z
·𝑜 u) = (w ·𝑜 v))) ↔ ((〈A, B〉 ∈ (𝜔 × N) ∧ 〈𝐶, 𝐷〉 ∈
(𝜔 × N)) ∧
(A ·𝑜 𝐷) = (B ·𝑜 𝐶)))) |
7 | | opexg 3955 |
. . 3
⊢
((A ∈ 𝜔 ∧
B ∈
N) → 〈A, B〉 ∈
V) |
8 | | opexg 3955 |
. . 3
⊢ ((𝐶 ∈ 𝜔 ∧
𝐷 ∈ N) → 〈𝐶, 𝐷〉 ∈
V) |
9 | | eleq1 2097 |
. . . . . 6
⊢ (x = 〈A,
B〉 → (x ∈ (𝜔
× N) ↔ 〈A,
B〉 ∈
(𝜔 × N))) |
10 | 9 | anbi1d 438 |
. . . . 5
⊢ (x = 〈A,
B〉 → ((x ∈ (𝜔
× N) ∧ y ∈ (𝜔
× N)) ↔ (〈A,
B〉 ∈
(𝜔 × N) ∧ y ∈ (𝜔
× N)))) |
11 | | eqeq1 2043 |
. . . . . . . 8
⊢ (x = 〈A,
B〉 → (x = 〈z,
w〉 ↔ 〈A, B〉 =
〈z, w〉)) |
12 | 11 | anbi1d 438 |
. . . . . . 7
⊢ (x = 〈A,
B〉 → ((x = 〈z,
w〉 ∧
y = 〈v, u〉)
↔ (〈A, B〉 = 〈z, w〉 ∧ y =
〈v, u〉))) |
13 | 12 | anbi1d 438 |
. . . . . 6
⊢ (x = 〈A,
B〉 → (((x = 〈z,
w〉 ∧
y = 〈v, u〉)
∧ (z
·𝑜 u) = (w ·𝑜 v)) ↔ ((〈A, B〉 =
〈z, w〉 ∧ y = 〈v,
u〉) ∧
(z ·𝑜 u) = (w
·𝑜 v)))) |
14 | 13 | 4exbidv 1747 |
. . . . 5
⊢ (x = 〈A,
B〉 → (∃z∃w∃v∃u((x = 〈z,
w〉 ∧
y = 〈v, u〉)
∧ (z
·𝑜 u) = (w ·𝑜 v)) ↔ ∃z∃w∃v∃u((〈A,
B〉 = 〈z, w〉 ∧ y =
〈v, u〉) ∧
(z ·𝑜 u) = (w
·𝑜 v)))) |
15 | 10, 14 | anbi12d 442 |
. . . 4
⊢ (x = 〈A,
B〉 → (((x ∈ (𝜔
× N) ∧ y ∈ (𝜔
× N)) ∧ ∃z∃w∃v∃u((x = 〈z,
w〉 ∧
y = 〈v, u〉)
∧ (z
·𝑜 u) = (w ·𝑜 v))) ↔ ((〈A, B〉 ∈ (𝜔 × N) ∧ y ∈ (𝜔 × N)) ∧ ∃z∃w∃v∃u((〈A,
B〉 = 〈z, w〉 ∧ y =
〈v, u〉) ∧
(z ·𝑜 u) = (w
·𝑜 v))))) |
16 | | eleq1 2097 |
. . . . . 6
⊢ (y = 〈𝐶, 𝐷〉 → (y ∈ (𝜔
× N) ↔ 〈𝐶, 𝐷〉 ∈
(𝜔 × N))) |
17 | 16 | anbi2d 437 |
. . . . 5
⊢ (y = 〈𝐶, 𝐷〉 → ((〈A, B〉 ∈ (𝜔 × N) ∧ y ∈ (𝜔 × N)) ↔
(〈A, B〉 ∈
(𝜔 × N) ∧
〈𝐶, 𝐷〉 ∈
(𝜔 × N)))) |
18 | | eqeq1 2043 |
. . . . . . . 8
⊢ (y = 〈𝐶, 𝐷〉 → (y = 〈v,
u〉 ↔ 〈𝐶, 𝐷〉 = 〈v, u〉)) |
19 | 18 | anbi2d 437 |
. . . . . . 7
⊢ (y = 〈𝐶, 𝐷〉 → ((〈A, B〉 =
〈z, w〉 ∧ y = 〈v,
u〉) ↔ (〈A, B〉 =
〈z, w〉 ∧
〈𝐶, 𝐷〉 = 〈v, u〉))) |
20 | 19 | anbi1d 438 |
. . . . . 6
⊢ (y = 〈𝐶, 𝐷〉 → (((〈A, B〉 =
〈z, w〉 ∧ y = 〈v,
u〉) ∧
(z ·𝑜 u) = (w
·𝑜 v)) ↔
((〈A, B〉 = 〈z, w〉 ∧ 〈𝐶, 𝐷〉 = 〈v, u〉)
∧ (z
·𝑜 u) = (w ·𝑜 v)))) |
21 | 20 | 4exbidv 1747 |
. . . . 5
⊢ (y = 〈𝐶, 𝐷〉 → (∃z∃w∃v∃u((〈A,
B〉 = 〈z, w〉 ∧ y =
〈v, u〉) ∧
(z ·𝑜 u) = (w
·𝑜 v)) ↔
∃z∃w∃v∃u((〈A,
B〉 = 〈z, w〉 ∧ 〈𝐶, 𝐷〉 = 〈v, u〉)
∧ (z
·𝑜 u) = (w ·𝑜 v)))) |
22 | 17, 21 | anbi12d 442 |
. . . 4
⊢ (y = 〈𝐶, 𝐷〉 → (((〈A, B〉 ∈ (𝜔 × N) ∧ y ∈ (𝜔 × N)) ∧ ∃z∃w∃v∃u((〈A,
B〉 = 〈z, w〉 ∧ y =
〈v, u〉) ∧
(z ·𝑜 u) = (w
·𝑜 v))) ↔
((〈A, B〉 ∈
(𝜔 × N) ∧
〈𝐶, 𝐷〉 ∈
(𝜔 × N)) ∧ ∃z∃w∃v∃u((〈A,
B〉 = 〈z, w〉 ∧ 〈𝐶, 𝐷〉 = 〈v, u〉)
∧ (z
·𝑜 u) = (w ·𝑜 v))))) |
23 | | df-enq0 6407 |
. . . 4
⊢
~Q0 = {〈x,
y〉 ∣ ((x ∈ (𝜔
× N) ∧ y ∈ (𝜔
× N)) ∧ ∃z∃w∃v∃u((x = 〈z,
w〉 ∧
y = 〈v, u〉)
∧ (z
·𝑜 u) = (w ·𝑜 v)))} |
24 | 15, 22, 23 | brabg 3997 |
. . 3
⊢
((〈A, B〉 ∈ V ∧ 〈𝐶, 𝐷〉 ∈
V) → (〈A, B〉 ~Q0 〈𝐶, 𝐷〉 ↔ ((〈A, B〉 ∈ (𝜔 × N) ∧ 〈𝐶, 𝐷〉 ∈
(𝜔 × N)) ∧ ∃z∃w∃v∃u((〈A,
B〉 = 〈z, w〉 ∧ 〈𝐶, 𝐷〉 = 〈v, u〉)
∧ (z
·𝑜 u) = (w ·𝑜 v))))) |
25 | 7, 8, 24 | syl2an 273 |
. 2
⊢
(((A ∈ 𝜔 ∧
B ∈
N) ∧ (𝐶 ∈
𝜔 ∧ 𝐷 ∈
N)) → (〈A, B〉 ~Q0 〈𝐶, 𝐷〉 ↔ ((〈A, B〉 ∈ (𝜔 × N) ∧ 〈𝐶, 𝐷〉 ∈
(𝜔 × N)) ∧ ∃z∃w∃v∃u((〈A,
B〉 = 〈z, w〉 ∧ 〈𝐶, 𝐷〉 = 〈v, u〉)
∧ (z
·𝑜 u) = (w ·𝑜 v))))) |
26 | | opelxpi 4319 |
. . . 4
⊢
((A ∈ 𝜔 ∧
B ∈
N) → 〈A, B〉 ∈
(𝜔 × N)) |
27 | | opelxpi 4319 |
. . . 4
⊢ ((𝐶 ∈ 𝜔 ∧
𝐷 ∈ N) → 〈𝐶, 𝐷〉 ∈
(𝜔 × N)) |
28 | 26, 27 | anim12i 321 |
. . 3
⊢
(((A ∈ 𝜔 ∧
B ∈
N) ∧ (𝐶 ∈
𝜔 ∧ 𝐷 ∈
N)) → (〈A, B〉 ∈
(𝜔 × N) ∧
〈𝐶, 𝐷〉 ∈
(𝜔 × N))) |
29 | 28 | biantrurd 289 |
. 2
⊢
(((A ∈ 𝜔 ∧
B ∈
N) ∧ (𝐶 ∈
𝜔 ∧ 𝐷 ∈
N)) → ((A
·𝑜 𝐷) = (B
·𝑜 𝐶) ↔ ((〈A, B〉 ∈ (𝜔 × N) ∧ 〈𝐶, 𝐷〉 ∈
(𝜔 × N)) ∧
(A ·𝑜 𝐷) = (B ·𝑜 𝐶)))) |
30 | 6, 25, 29 | 3bitr4d 209 |
1
⊢
(((A ∈ 𝜔 ∧
B ∈
N) ∧ (𝐶 ∈
𝜔 ∧ 𝐷 ∈
N)) → (〈A, B〉 ~Q0 〈𝐶, 𝐷〉 ↔ (A ·𝑜 𝐷) = (B
·𝑜 𝐶))) |