Proof of Theorem cgsex4g
Step | Hyp | Ref
| Expression |
1 | | cgsex4g.2 |
. . . . 5
⊢ (χ → (φ ↔ ψ)) |
2 | 1 | biimpa 470 |
. . . 4
⊢ ((χ ∧ φ) → ψ) |
3 | 2 | exlimivv 1635 |
. . 3
⊢ (∃z∃w(χ ∧ φ) → ψ) |
4 | 3 | exlimivv 1635 |
. 2
⊢ (∃x∃y∃z∃w(χ ∧ φ) → ψ) |
5 | | elisset 2869 |
. . . . . . . 8
⊢ (A ∈ R → ∃x x = A) |
6 | | elisset 2869 |
. . . . . . . 8
⊢ (B ∈ S → ∃y y = B) |
7 | 5, 6 | anim12i 549 |
. . . . . . 7
⊢ ((A ∈ R ∧ B ∈ S) → (∃x x = A ∧ ∃y y = B)) |
8 | | eeanv 1913 |
. . . . . . 7
⊢ (∃x∃y(x = A ∧ y = B) ↔ (∃x x = A ∧ ∃y y = B)) |
9 | 7, 8 | sylibr 203 |
. . . . . 6
⊢ ((A ∈ R ∧ B ∈ S) → ∃x∃y(x = A ∧ y = B)) |
10 | | elisset 2869 |
. . . . . . . 8
⊢ (C ∈ R → ∃z z = C) |
11 | | elisset 2869 |
. . . . . . . 8
⊢ (D ∈ S → ∃w w = D) |
12 | 10, 11 | anim12i 549 |
. . . . . . 7
⊢ ((C ∈ R ∧ D ∈ S) → (∃z z = C ∧ ∃w w = D)) |
13 | | eeanv 1913 |
. . . . . . 7
⊢ (∃z∃w(z = C ∧ w = D) ↔ (∃z z = C ∧ ∃w w = D)) |
14 | 12, 13 | sylibr 203 |
. . . . . 6
⊢ ((C ∈ R ∧ D ∈ S) → ∃z∃w(z = C ∧ w = D)) |
15 | 9, 14 | anim12i 549 |
. . . . 5
⊢ (((A ∈ R ∧ B ∈ S) ∧ (C ∈ R ∧ D ∈ S)) → (∃x∃y(x = A ∧ y = B) ∧ ∃z∃w(z = C ∧ w = D))) |
16 | | ee4anv 1915 |
. . . . 5
⊢ (∃x∃y∃z∃w((x = A ∧ y = B) ∧ (z = C ∧ w = D)) ↔ (∃x∃y(x = A ∧ y = B) ∧ ∃z∃w(z = C ∧ w = D))) |
17 | 15, 16 | sylibr 203 |
. . . 4
⊢ (((A ∈ R ∧ B ∈ S) ∧ (C ∈ R ∧ D ∈ S)) → ∃x∃y∃z∃w((x = A ∧ y = B) ∧ (z = C ∧ w = D))) |
18 | | cgsex4g.1 |
. . . . . 6
⊢ (((x = A ∧ y = B) ∧ (z = C ∧ w = D)) → χ) |
19 | 18 | 2eximi 1577 |
. . . . 5
⊢ (∃z∃w((x = A ∧ y = B) ∧ (z = C ∧ w = D)) → ∃z∃wχ) |
20 | 19 | 2eximi 1577 |
. . . 4
⊢ (∃x∃y∃z∃w((x = A ∧ y = B) ∧ (z = C ∧ w = D)) → ∃x∃y∃z∃wχ) |
21 | 17, 20 | syl 15 |
. . 3
⊢ (((A ∈ R ∧ B ∈ S) ∧ (C ∈ R ∧ D ∈ S)) → ∃x∃y∃z∃wχ) |
22 | 1 | biimprcd 216 |
. . . . . 6
⊢ (ψ → (χ → φ)) |
23 | 22 | ancld 536 |
. . . . 5
⊢ (ψ → (χ → (χ ∧ φ))) |
24 | 23 | 2eximdv 1624 |
. . . 4
⊢ (ψ → (∃z∃wχ → ∃z∃w(χ ∧ φ))) |
25 | 24 | 2eximdv 1624 |
. . 3
⊢ (ψ → (∃x∃y∃z∃wχ → ∃x∃y∃z∃w(χ ∧ φ))) |
26 | 21, 25 | syl5com 26 |
. 2
⊢ (((A ∈ R ∧ B ∈ S) ∧ (C ∈ R ∧ D ∈ S)) → (ψ → ∃x∃y∃z∃w(χ ∧ φ))) |
27 | 4, 26 | impbid2 195 |
1
⊢ (((A ∈ R ∧ B ∈ S) ∧ (C ∈ R ∧ D ∈ S)) → (∃x∃y∃z∃w(χ ∧ φ) ↔ ψ)) |