Step | Hyp | Ref
| Expression |
1 | | opbrop.1 |
. . . 4
⊢ (((z = A ∧ w = B) ∧ (v = C ∧ u = D)) → (φ ↔ ψ)) |
2 | 1 | copsex4g 4611 |
. . 3
⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → (∃z∃w∃v∃u((⟨A, B⟩ = ⟨z, w⟩ ∧ ⟨C, D⟩ = ⟨v, u⟩) ∧ φ) ↔ ψ)) |
3 | 2 | anbi2d 684 |
. 2
⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → (((⟨A, B⟩ ∈ (S ×
S) ∧ ⟨C, D⟩ ∈ (S ×
S)) ∧
∃z∃w∃v∃u((⟨A, B⟩ = ⟨z, w⟩ ∧ ⟨C, D⟩ = ⟨v, u⟩) ∧ φ)) ↔ ((⟨A, B⟩ ∈ (S ×
S) ∧ ⟨C, D⟩ ∈ (S ×
S)) ∧
ψ))) |
4 | | opexg 4588 |
. . 3
⊢ ((A ∈ S ∧ B ∈ S) → ⟨A, B⟩ ∈ V) |
5 | | opexg 4588 |
. . 3
⊢ ((C ∈ S ∧ D ∈ S) → ⟨C, D⟩ ∈ V) |
6 | | eleq1 2413 |
. . . . . 6
⊢ (x = ⟨A, B⟩ → (x
∈ (S
× S) ↔ ⟨A, B⟩ ∈ (S ×
S))) |
7 | 6 | anbi1d 685 |
. . . . 5
⊢ (x = ⟨A, B⟩ → ((x
∈ (S
× S) ∧ y ∈ (S ×
S)) ↔ (⟨A, B⟩ ∈ (S ×
S) ∧
y ∈
(S × S)))) |
8 | | eqeq1 2359 |
. . . . . . . 8
⊢ (x = ⟨A, B⟩ → (x =
⟨z,
w⟩ ↔
⟨A,
B⟩ =
⟨z,
w⟩)) |
9 | 8 | anbi1d 685 |
. . . . . . 7
⊢ (x = ⟨A, B⟩ → ((x =
⟨z,
w⟩ ∧ y = ⟨v, u⟩) ↔ (⟨A, B⟩ = ⟨z, w⟩ ∧ y = ⟨v, u⟩))) |
10 | 9 | anbi1d 685 |
. . . . . 6
⊢ (x = ⟨A, B⟩ → (((x =
⟨z,
w⟩ ∧ y = ⟨v, u⟩) ∧ φ) ↔
((⟨A,
B⟩ =
⟨z,
w⟩ ∧ y = ⟨v, u⟩) ∧ φ))) |
11 | 10 | 4exbidv 1630 |
. . . . 5
⊢ (x = ⟨A, B⟩ → (∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ φ) ↔ ∃z∃w∃v∃u((⟨A, B⟩ = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ φ))) |
12 | 7, 11 | anbi12d 691 |
. . . 4
⊢ (x = ⟨A, B⟩ → (((x
∈ (S
× S) ∧ y ∈ (S ×
S)) ∧
∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ φ)) ↔ ((⟨A, B⟩ ∈ (S ×
S) ∧
y ∈
(S × S)) ∧ ∃z∃w∃v∃u((⟨A, B⟩ = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ φ)))) |
13 | | eleq1 2413 |
. . . . . 6
⊢ (y = ⟨C, D⟩ → (y
∈ (S
× S) ↔ ⟨C, D⟩ ∈ (S ×
S))) |
14 | 13 | anbi2d 684 |
. . . . 5
⊢ (y = ⟨C, D⟩ → ((⟨A, B⟩ ∈ (S ×
S) ∧
y ∈
(S × S)) ↔ (⟨A, B⟩ ∈ (S ×
S) ∧ ⟨C, D⟩ ∈ (S ×
S)))) |
15 | | eqeq1 2359 |
. . . . . . . 8
⊢ (y = ⟨C, D⟩ → (y =
⟨v,
u⟩ ↔
⟨C,
D⟩ =
⟨v,
u⟩)) |
16 | 15 | anbi2d 684 |
. . . . . . 7
⊢ (y = ⟨C, D⟩ → ((⟨A, B⟩ = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ↔ (⟨A, B⟩ = ⟨z, w⟩ ∧ ⟨C, D⟩ = ⟨v, u⟩))) |
17 | 16 | anbi1d 685 |
. . . . . 6
⊢ (y = ⟨C, D⟩ → (((⟨A, B⟩ = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ φ) ↔
((⟨A,
B⟩ =
⟨z,
w⟩ ∧ ⟨C, D⟩ = ⟨v, u⟩) ∧ φ))) |
18 | 17 | 4exbidv 1630 |
. . . . 5
⊢ (y = ⟨C, D⟩ → (∃z∃w∃v∃u((⟨A, B⟩ = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ φ) ↔
∃z∃w∃v∃u((⟨A, B⟩ = ⟨z, w⟩ ∧ ⟨C, D⟩ = ⟨v, u⟩) ∧ φ))) |
19 | 14, 18 | anbi12d 691 |
. . . 4
⊢ (y = ⟨C, D⟩ → (((⟨A, B⟩ ∈ (S ×
S) ∧
y ∈
(S × S)) ∧ ∃z∃w∃v∃u((⟨A, B⟩ = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ φ)) ↔
((⟨A,
B⟩ ∈ (S ×
S) ∧ ⟨C, D⟩ ∈ (S ×
S)) ∧
∃z∃w∃v∃u((⟨A, B⟩ = ⟨z, w⟩ ∧ ⟨C, D⟩ = ⟨v, u⟩) ∧ φ)))) |
20 | | opbrop.2 |
. . . 4
⊢ R = {⟨x, y⟩ ∣ ((x ∈ (S × S)
∧ y ∈ (S ×
S)) ∧
∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ φ))} |
21 | 12, 19, 20 | brabg 4707 |
. . 3
⊢ ((⟨A, B⟩ ∈ V ∧ ⟨C, D⟩ ∈ V) → (⟨A, B⟩R⟨C, D⟩ ↔ ((⟨A, B⟩ ∈ (S ×
S) ∧ ⟨C, D⟩ ∈ (S ×
S)) ∧
∃z∃w∃v∃u((⟨A, B⟩ = ⟨z, w⟩ ∧ ⟨C, D⟩ = ⟨v, u⟩) ∧ φ)))) |
22 | 4, 5, 21 | syl2an 463 |
. 2
⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → (⟨A, B⟩R⟨C, D⟩ ↔ ((⟨A, B⟩ ∈ (S ×
S) ∧ ⟨C, D⟩ ∈ (S ×
S)) ∧
∃z∃w∃v∃u((⟨A, B⟩ = ⟨z, w⟩ ∧ ⟨C, D⟩ = ⟨v, u⟩) ∧ φ)))) |
23 | | opelxp 4812 |
. . . . 5
⊢ (⟨A, B⟩ ∈ (S ×
S) ↔ (A ∈ S ∧ B ∈ S)) |
24 | | opelxp 4812 |
. . . . 5
⊢ (⟨C, D⟩ ∈ (S ×
S) ↔ (C ∈ S ∧ D ∈ S)) |
25 | 23, 24 | anbi12i 678 |
. . . 4
⊢ ((⟨A, B⟩ ∈ (S ×
S) ∧ ⟨C, D⟩ ∈ (S ×
S)) ↔ ((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S))) |
26 | 25 | biimpri 197 |
. . 3
⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → (⟨A, B⟩ ∈ (S ×
S) ∧ ⟨C, D⟩ ∈ (S ×
S))) |
27 | 26 | biantrurd 494 |
. 2
⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → (ψ ↔ ((⟨A, B⟩ ∈ (S ×
S) ∧ ⟨C, D⟩ ∈ (S ×
S)) ∧
ψ))) |
28 | 3, 22, 27 | 3bitr4d 276 |
1
⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → (⟨A, B⟩R⟨C, D⟩ ↔ ψ)) |