Step | Hyp | Ref
| Expression |
1 | | cgsex4g.2 |
. . . . 5
⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
2 | 1 | biimpa 480 |
. . . 4
⊢ ((𝜒 ∧ 𝜑) → 𝜓) |
3 | 2 | exlimivv 1938 |
. . 3
⊢
(∃𝑧∃𝑤(𝜒 ∧ 𝜑) → 𝜓) |
4 | 3 | exlimivv 1938 |
. 2
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) → 𝜓) |
5 | | elisset 2814 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑅 → ∃𝑥 𝑥 = 𝐴) |
6 | | elisset 2814 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑆 → ∃𝑦 𝑦 = 𝐵) |
7 | 5, 6 | anim12i 616 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)) |
8 | | exdistrv 1962 |
. . . . . . 7
⊢
(∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)) |
9 | 7, 8 | sylibr 237 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
10 | | elisset 2814 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑅 → ∃𝑧 𝑧 = 𝐶) |
11 | | elisset 2814 |
. . . . . . . 8
⊢ (𝐷 ∈ 𝑆 → ∃𝑤 𝑤 = 𝐷) |
12 | 10, 11 | anim12i 616 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆) → (∃𝑧 𝑧 = 𝐶 ∧ ∃𝑤 𝑤 = 𝐷)) |
13 | | exdistrv 1962 |
. . . . . . 7
⊢
(∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷) ↔ (∃𝑧 𝑧 = 𝐶 ∧ ∃𝑤 𝑤 = 𝐷)) |
14 | 12, 13 | sylibr 237 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆) → ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) |
15 | 9, 14 | anim12i 616 |
. . . . 5
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
16 | | eqeq1 2742 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑣 → (𝑧 = 𝐶 ↔ 𝑣 = 𝐶)) |
17 | 16 | anbi1d 633 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑣 → ((𝑧 = 𝐶 ∧ 𝑤 = 𝐷) ↔ (𝑣 = 𝐶 ∧ 𝑤 = 𝐷))) |
18 | 17 | anbi2d 632 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑣 → (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑣 = 𝐶 ∧ 𝑤 = 𝐷)))) |
19 | 18 | exbidv 1927 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑣 → (∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑣 = 𝐶 ∧ 𝑤 = 𝐷)))) |
20 | 19 | notbid 321 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑣 → (¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑣 = 𝐶 ∧ 𝑤 = 𝐷)))) |
21 | 20 | alcomiw 2054 |
. . . . . . . . . 10
⊢
(∀𝑦∀𝑧 ¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → ∀𝑧∀𝑦 ¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
22 | | eqeq1 2742 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑣 → (𝑦 = 𝐵 ↔ 𝑣 = 𝐵)) |
23 | 22 | anbi2d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑣 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 = 𝐴 ∧ 𝑣 = 𝐵))) |
24 | 23 | anbi1d 633 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑣 → (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ((𝑥 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)))) |
25 | 24 | exbidv 1927 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑣 → (∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ∃𝑤((𝑥 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)))) |
26 | 25 | notbid 321 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑣 → (¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)))) |
27 | 26 | alcomiw 2054 |
. . . . . . . . . 10
⊢
(∀𝑧∀𝑦 ¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → ∀𝑦∀𝑧 ¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
28 | 21, 27 | impbii 212 |
. . . . . . . . 9
⊢
(∀𝑦∀𝑧 ¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ∀𝑧∀𝑦 ¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
29 | 28 | notbii 323 |
. . . . . . . 8
⊢ (¬
∀𝑦∀𝑧 ¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ¬ ∀𝑧∀𝑦 ¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
30 | | 2exnaln 1835 |
. . . . . . . 8
⊢
(∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ¬ ∀𝑦∀𝑧 ¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
31 | | 2exnaln 1835 |
. . . . . . . 8
⊢
(∃𝑧∃𝑦∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ¬ ∀𝑧∀𝑦 ¬ ∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
32 | 29, 30, 31 | 3bitr4i 306 |
. . . . . . 7
⊢
(∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ∃𝑧∃𝑦∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
33 | 32 | exbii 1854 |
. . . . . 6
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ∃𝑥∃𝑧∃𝑦∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
34 | | 4exdistrv 1963 |
. . . . . 6
⊢
(∃𝑥∃𝑧∃𝑦∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
35 | 33, 34 | bitri 278 |
. . . . 5
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
36 | 15, 35 | sylibr 237 |
. . . 4
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → ∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
37 | | cgsex4g.1 |
. . . . . 6
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → 𝜒) |
38 | 37 | 2eximi 1842 |
. . . . 5
⊢
(∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → ∃𝑧∃𝑤𝜒) |
39 | 38 | 2eximi 1842 |
. . . 4
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → ∃𝑥∃𝑦∃𝑧∃𝑤𝜒) |
40 | 36, 39 | syl 17 |
. . 3
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → ∃𝑥∃𝑦∃𝑧∃𝑤𝜒) |
41 | 1 | biimprcd 253 |
. . . . . 6
⊢ (𝜓 → (𝜒 → 𝜑)) |
42 | 41 | ancld 554 |
. . . . 5
⊢ (𝜓 → (𝜒 → (𝜒 ∧ 𝜑))) |
43 | 42 | 2eximdv 1925 |
. . . 4
⊢ (𝜓 → (∃𝑧∃𝑤𝜒 → ∃𝑧∃𝑤(𝜒 ∧ 𝜑))) |
44 | 43 | 2eximdv 1925 |
. . 3
⊢ (𝜓 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜒 → ∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑))) |
45 | 40, 44 | syl5com 31 |
. 2
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (𝜓 → ∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑))) |
46 | 4, 45 | impbid2 229 |
1
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) ↔ 𝜓)) |