Proof of Theorem opbrop
Step | Hyp | Ref
| Expression |
1 | | opbrop.1 |
. . . 4
⊢ (((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ (𝑣 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝜑 ↔ 𝜓)) |
2 | 1 | copsex4g 3984 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (∃𝑧∃𝑤∃𝑣∃𝑢((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑣, 𝑢〉) ∧ 𝜑) ↔ 𝜓)) |
3 | 2 | anbi2d 437 |
. 2
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (((〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ∧ 〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑣, 𝑢〉) ∧ 𝜑)) ↔ ((〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ∧ 〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆)) ∧ 𝜓))) |
4 | | elex 2566 |
. . . 4
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ V) |
5 | | elex 2566 |
. . . 4
⊢ (𝐵 ∈ 𝑆 → 𝐵 ∈ V) |
6 | | opexgOLD 3965 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 〈𝐴, 𝐵〉 ∈ V) |
7 | 4, 5, 6 | syl2an 273 |
. . 3
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 〈𝐴, 𝐵〉 ∈ V) |
8 | | elex 2566 |
. . . 4
⊢ (𝐶 ∈ 𝑆 → 𝐶 ∈ V) |
9 | | elex 2566 |
. . . 4
⊢ (𝐷 ∈ 𝑆 → 𝐷 ∈ V) |
10 | | opexgOLD 3965 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 〈𝐶, 𝐷〉 ∈ V) |
11 | 8, 9, 10 | syl2an 273 |
. . 3
⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 〈𝐶, 𝐷〉 ∈ V) |
12 | | eleq1 2100 |
. . . . . 6
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (𝑥 ∈ (𝑆 × 𝑆) ↔ 〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆))) |
13 | 12 | anbi1d 438 |
. . . . 5
⊢ (𝑥 = 〈𝐴, 𝐵〉 → ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ↔ (〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)))) |
14 | | eqeq1 2046 |
. . . . . . . 8
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (𝑥 = 〈𝑧, 𝑤〉 ↔ 〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉)) |
15 | 14 | anbi1d 438 |
. . . . . . 7
⊢ (𝑥 = 〈𝐴, 𝐵〉 → ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ↔ (〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉))) |
16 | 15 | anbi1d 438 |
. . . . . 6
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ 𝜑) ↔ ((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ 𝜑))) |
17 | 16 | 4exbidv 1750 |
. . . . 5
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ 𝜑) ↔ ∃𝑧∃𝑤∃𝑣∃𝑢((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ 𝜑))) |
18 | 13, 17 | anbi12d 442 |
. . . 4
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ 𝜑)) ↔ ((〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ 𝜑)))) |
19 | | eleq1 2100 |
. . . . . 6
⊢ (𝑦 = 〈𝐶, 𝐷〉 → (𝑦 ∈ (𝑆 × 𝑆) ↔ 〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆))) |
20 | 19 | anbi2d 437 |
. . . . 5
⊢ (𝑦 = 〈𝐶, 𝐷〉 → ((〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ↔ (〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ∧ 〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆)))) |
21 | | eqeq1 2046 |
. . . . . . . 8
⊢ (𝑦 = 〈𝐶, 𝐷〉 → (𝑦 = 〈𝑣, 𝑢〉 ↔ 〈𝐶, 𝐷〉 = 〈𝑣, 𝑢〉)) |
22 | 21 | anbi2d 437 |
. . . . . . 7
⊢ (𝑦 = 〈𝐶, 𝐷〉 → ((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ↔ (〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑣, 𝑢〉))) |
23 | 22 | anbi1d 438 |
. . . . . 6
⊢ (𝑦 = 〈𝐶, 𝐷〉 → (((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ 𝜑) ↔ ((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑣, 𝑢〉) ∧ 𝜑))) |
24 | 23 | 4exbidv 1750 |
. . . . 5
⊢ (𝑦 = 〈𝐶, 𝐷〉 → (∃𝑧∃𝑤∃𝑣∃𝑢((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ 𝜑) ↔ ∃𝑧∃𝑤∃𝑣∃𝑢((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑣, 𝑢〉) ∧ 𝜑))) |
25 | 20, 24 | anbi12d 442 |
. . . 4
⊢ (𝑦 = 〈𝐶, 𝐷〉 → (((〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ 𝜑)) ↔ ((〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ∧ 〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑣, 𝑢〉) ∧ 𝜑)))) |
26 | | opbrop.2 |
. . . 4
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ 𝜑))} |
27 | 18, 25, 26 | brabg 4006 |
. . 3
⊢
((〈𝐴, 𝐵〉 ∈ V ∧
〈𝐶, 𝐷〉 ∈ V) → (〈𝐴, 𝐵〉𝑅〈𝐶, 𝐷〉 ↔ ((〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ∧ 〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑣, 𝑢〉) ∧ 𝜑)))) |
28 | 7, 11, 27 | syl2an 273 |
. 2
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈𝐴, 𝐵〉𝑅〈𝐶, 𝐷〉 ↔ ((〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ∧ 〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑣, 𝑢〉) ∧ 𝜑)))) |
29 | | opelxpi 4376 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆)) |
30 | | opelxpi 4376 |
. . . 4
⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆)) |
31 | 29, 30 | anim12i 321 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ∧ 〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆))) |
32 | 31 | biantrurd 289 |
. 2
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝜓 ↔ ((〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ∧ 〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆)) ∧ 𝜓))) |
33 | 3, 28, 32 | 3bitr4d 209 |
1
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈𝐴, 𝐵〉𝑅〈𝐶, 𝐷〉 ↔ 𝜓)) |