Proof of Theorem cgsex4gOLD
Step | Hyp | Ref
| Expression |
1 | | cgsex4gOLD.2 |
. . . . 5
⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
2 | 1 | biimpa 481 |
. . . 4
⊢ ((𝜒 ∧ 𝜑) → 𝜓) |
3 | 2 | exlimivv 1934 |
. . 3
⊢
(∃𝑧∃𝑤(𝜒 ∧ 𝜑) → 𝜓) |
4 | 3 | exlimivv 1934 |
. 2
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) → 𝜓) |
5 | | elisset 3420 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑅 → ∃𝑥 𝑥 = 𝐴) |
6 | | elisset 3420 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑆 → ∃𝑦 𝑦 = 𝐵) |
7 | 5, 6 | anim12i 616 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)) |
8 | | exdistrv 1957 |
. . . . . . 7
⊢
(∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)) |
9 | 7, 8 | sylibr 237 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
10 | | elisset 3420 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑅 → ∃𝑧 𝑧 = 𝐶) |
11 | | elisset 3420 |
. . . . . . . 8
⊢ (𝐷 ∈ 𝑆 → ∃𝑤 𝑤 = 𝐷) |
12 | 10, 11 | anim12i 616 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆) → (∃𝑧 𝑧 = 𝐶 ∧ ∃𝑤 𝑤 = 𝐷)) |
13 | | exdistrv 1957 |
. . . . . . 7
⊢
(∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷) ↔ (∃𝑧 𝑧 = 𝐶 ∧ ∃𝑤 𝑤 = 𝐷)) |
14 | 12, 13 | sylibr 237 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆) → ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) |
15 | 9, 14 | anim12i 616 |
. . . . 5
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
16 | | excom 2167 |
. . . . . . 7
⊢
(∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ∃𝑧∃𝑦∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
17 | 16 | exbii 1850 |
. . . . . 6
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ∃𝑥∃𝑧∃𝑦∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
18 | | 4exdistrv 1958 |
. . . . . 6
⊢
(∃𝑥∃𝑧∃𝑦∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
19 | 17, 18 | bitri 278 |
. . . . 5
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
20 | 15, 19 | sylibr 237 |
. . . 4
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → ∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
21 | | cgsex4gOLD.1 |
. . . . . 6
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → 𝜒) |
22 | 21 | 2eximi 1838 |
. . . . 5
⊢
(∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → ∃𝑧∃𝑤𝜒) |
23 | 22 | 2eximi 1838 |
. . . 4
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → ∃𝑥∃𝑦∃𝑧∃𝑤𝜒) |
24 | 20, 23 | syl 17 |
. . 3
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → ∃𝑥∃𝑦∃𝑧∃𝑤𝜒) |
25 | 1 | biimprcd 253 |
. . . . . 6
⊢ (𝜓 → (𝜒 → 𝜑)) |
26 | 25 | ancld 555 |
. . . . 5
⊢ (𝜓 → (𝜒 → (𝜒 ∧ 𝜑))) |
27 | 26 | 2eximdv 1921 |
. . . 4
⊢ (𝜓 → (∃𝑧∃𝑤𝜒 → ∃𝑧∃𝑤(𝜒 ∧ 𝜑))) |
28 | 27 | 2eximdv 1921 |
. . 3
⊢ (𝜓 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜒 → ∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑))) |
29 | 24, 28 | syl5com 31 |
. 2
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (𝜓 → ∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑))) |
30 | 4, 29 | impbid2 229 |
1
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) ↔ 𝜓)) |