Proof of Theorem br4
Step | Hyp | Ref
| Expression |
1 | | opex 5363 |
. . 3
⊢
〈𝐴, 𝐵〉 ∈ V |
2 | | opex 5363 |
. . 3
⊢
〈𝐶, 𝐷〉 ∈ V |
3 | | eqeq1 2742 |
. . . . . . 7
⊢ (𝑝 = 〈𝐴, 𝐵〉 → (𝑝 = 〈𝑎, 𝑏〉 ↔ 〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉)) |
4 | 3 | 3anbi1d 1442 |
. . . . . 6
⊢ (𝑝 = 〈𝐴, 𝐵〉 → ((𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑))) |
5 | 4 | rexbidv 3224 |
. . . . 5
⊢ (𝑝 = 〈𝐴, 𝐵〉 → (∃𝑑 ∈ 𝑃 (𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑))) |
6 | 5 | 2rexbidv 3227 |
. . . 4
⊢ (𝑝 = 〈𝐴, 𝐵〉 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑))) |
7 | 6 | 2rexbidv 3227 |
. . 3
⊢ (𝑝 = 〈𝐴, 𝐵〉 → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑))) |
8 | | eqeq1 2742 |
. . . . . . 7
⊢ (𝑞 = 〈𝐶, 𝐷〉 → (𝑞 = 〈𝑐, 𝑑〉 ↔ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉)) |
9 | 8 | 3anbi2d 1443 |
. . . . . 6
⊢ (𝑞 = 〈𝐶, 𝐷〉 → ((〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑))) |
10 | 9 | rexbidv 3224 |
. . . . 5
⊢ (𝑞 = 〈𝐶, 𝐷〉 → (∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑))) |
11 | 10 | 2rexbidv 3227 |
. . . 4
⊢ (𝑞 = 〈𝐶, 𝐷〉 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑))) |
12 | 11 | 2rexbidv 3227 |
. . 3
⊢ (𝑞 = 〈𝐶, 𝐷〉 → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑))) |
13 | | br4.6 |
. . 3
⊢ 𝑅 = {〈𝑝, 𝑞〉 ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑)} |
14 | 1, 2, 7, 12, 13 | brab 5439 |
. 2
⊢
(〈𝐴, 𝐵〉𝑅〈𝐶, 𝐷〉 ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑)) |
15 | | vex 3425 |
. . . . . . . . . . . 12
⊢ 𝑎 ∈ V |
16 | | vex 3425 |
. . . . . . . . . . . 12
⊢ 𝑏 ∈ V |
17 | 15, 16 | opth 5375 |
. . . . . . . . . . 11
⊢
(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) |
18 | | br4.1 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) |
19 | | br4.2 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) |
20 | 18, 19 | sylan9bb 513 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝜑 ↔ 𝜒)) |
21 | 17, 20 | sylbi 220 |
. . . . . . . . . 10
⊢
(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 → (𝜑 ↔ 𝜒)) |
22 | 21 | eqcoms 2746 |
. . . . . . . . 9
⊢
(〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 → (𝜑 ↔ 𝜒)) |
23 | | vex 3425 |
. . . . . . . . . . . 12
⊢ 𝑐 ∈ V |
24 | | vex 3425 |
. . . . . . . . . . . 12
⊢ 𝑑 ∈ V |
25 | 23, 24 | opth 5375 |
. . . . . . . . . . 11
⊢
(〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ↔ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) |
26 | | br4.3 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) |
27 | | br4.4 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) |
28 | 26, 27 | sylan9bb 513 |
. . . . . . . . . . 11
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (𝜒 ↔ 𝜏)) |
29 | 25, 28 | sylbi 220 |
. . . . . . . . . 10
⊢
(〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 → (𝜒 ↔ 𝜏)) |
30 | 29 | eqcoms 2746 |
. . . . . . . . 9
⊢
(〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 → (𝜒 ↔ 𝜏)) |
31 | 22, 30 | sylan9bb 513 |
. . . . . . . 8
⊢
((〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉) → (𝜑 ↔ 𝜏)) |
32 | 31 | biimp3a 1471 |
. . . . . . 7
⊢
((〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑) → 𝜏) |
33 | 32 | a1i 11 |
. . . . . 6
⊢
(((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ 𝑑 ∈ 𝑃) → ((〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑) → 𝜏)) |
34 | 33 | rexlimdva 3211 |
. . . . 5
⊢ ((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) → (∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑) → 𝜏)) |
35 | 34 | rexlimdvva 3221 |
. . . 4
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑) → 𝜏)) |
36 | 35 | rexlimdvva 3221 |
. . 3
⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑) → 𝜏)) |
37 | | simpl1 1193 |
. . . . 5
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝑋 ∈ 𝑆) |
38 | | simpl2l 1228 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐴 ∈ 𝑄) |
39 | | simpl2r 1229 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐵 ∈ 𝑄) |
40 | | simpl3l 1230 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐶 ∈ 𝑄) |
41 | | simpl3r 1231 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐷 ∈ 𝑄) |
42 | | eqidd 2739 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉) |
43 | | eqidd 2739 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 〈𝐶, 𝐷〉 = 〈𝐶, 𝐷〉) |
44 | | simpr 488 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝜏) |
45 | | opeq1 4799 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐶 → 〈𝑐, 𝑑〉 = 〈𝐶, 𝑑〉) |
46 | 45 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → (〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ↔ 〈𝐶, 𝐷〉 = 〈𝐶, 𝑑〉)) |
47 | 46, 26 | 3anbi23d 1441 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → ((〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜒) ↔ (〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉 = 〈𝐶, 𝑑〉 ∧ 𝜃))) |
48 | | opeq2 4800 |
. . . . . . . . . 10
⊢ (𝑑 = 𝐷 → 〈𝐶, 𝑑〉 = 〈𝐶, 𝐷〉) |
49 | 48 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → (〈𝐶, 𝐷〉 = 〈𝐶, 𝑑〉 ↔ 〈𝐶, 𝐷〉 = 〈𝐶, 𝐷〉)) |
50 | 49, 27 | 3anbi23d 1441 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → ((〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉 = 〈𝐶, 𝑑〉 ∧ 𝜃) ↔ (〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉 = 〈𝐶, 𝐷〉 ∧ 𝜏))) |
51 | 47, 50 | rspc2ev 3562 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ (〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉 = 〈𝐶, 𝐷〉 ∧ 𝜏)) → ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜒)) |
52 | 40, 41, 42, 43, 44, 51 | syl113anc 1384 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜒)) |
53 | | opeq1 4799 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) |
54 | 53 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ↔ 〈𝐴, 𝐵〉 = 〈𝐴, 𝑏〉)) |
55 | 54, 18 | 3anbi13d 1440 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → ((〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ (〈𝐴, 𝐵〉 = 〈𝐴, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜓))) |
56 | 55 | 2rexbidv 3227 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝐴, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜓))) |
57 | | opeq2 4800 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → 〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉) |
58 | 57 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (〈𝐴, 𝐵〉 = 〈𝐴, 𝑏〉 ↔ 〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉)) |
59 | 58, 19 | 3anbi13d 1440 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → ((〈𝐴, 𝐵〉 = 〈𝐴, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜓) ↔ (〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜒))) |
60 | 59 | 2rexbidv 3227 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝐴, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜓) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜒))) |
61 | 56, 60 | rspc2ev 3562 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜒)) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑)) |
62 | 38, 39, 52, 61 | syl3anc 1373 |
. . . . 5
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑)) |
63 | | br4.5 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) |
64 | 63 | rexeqdv 3339 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑))) |
65 | 63, 64 | rexeqbidv 3327 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑))) |
66 | 63, 65 | rexeqbidv 3327 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑))) |
67 | 63, 66 | rexeqbidv 3327 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑))) |
68 | 67 | rspcev 3550 |
. . . . 5
⊢ ((𝑋 ∈ 𝑆 ∧ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑)) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑)) |
69 | 37, 62, 68 | syl2anc 587 |
. . . 4
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑)) |
70 | 69 | ex 416 |
. . 3
⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (𝜏 → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑))) |
71 | 36, 70 | impbid 215 |
. 2
⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ∧ 𝜑) ↔ 𝜏)) |
72 | 14, 71 | syl5bb 286 |
1
⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (〈𝐴, 𝐵〉𝑅〈𝐶, 𝐷〉 ↔ 𝜏)) |