Proof of Theorem vtocl3gaf
Step | Hyp | Ref
| Expression |
1 | | vtocl3gaf.a |
. . 3
⊢
ℲxA |
2 | | vtocl3gaf.b |
. . 3
⊢
ℲyA |
3 | | vtocl3gaf.c |
. . 3
⊢
ℲzA |
4 | | vtocl3gaf.d |
. . 3
⊢
ℲyB |
5 | | vtocl3gaf.e |
. . 3
⊢
ℲzB |
6 | | vtocl3gaf.f |
. . 3
⊢
ℲzC |
7 | 1 | nfel1 2499 |
. . . . 5
⊢ Ⅎx A ∈ R |
8 | | nfv 1619 |
. . . . 5
⊢ Ⅎx y ∈ S |
9 | | nfv 1619 |
. . . . 5
⊢ Ⅎx z ∈ T |
10 | 7, 8, 9 | nf3an 1827 |
. . . 4
⊢ Ⅎx(A ∈ R ∧ y ∈ S ∧ z ∈ T) |
11 | | vtocl3gaf.1 |
. . . 4
⊢ Ⅎxψ |
12 | 10, 11 | nfim 1813 |
. . 3
⊢ Ⅎx((A ∈ R ∧ y ∈ S ∧ z ∈ T) →
ψ) |
13 | 2 | nfel1 2499 |
. . . . 5
⊢ Ⅎy A ∈ R |
14 | 4 | nfel1 2499 |
. . . . 5
⊢ Ⅎy B ∈ S |
15 | | nfv 1619 |
. . . . 5
⊢ Ⅎy z ∈ T |
16 | 13, 14, 15 | nf3an 1827 |
. . . 4
⊢ Ⅎy(A ∈ R ∧ B ∈ S ∧ z ∈ T) |
17 | | vtocl3gaf.2 |
. . . 4
⊢ Ⅎyχ |
18 | 16, 17 | nfim 1813 |
. . 3
⊢ Ⅎy((A ∈ R ∧ B ∈ S ∧ z ∈ T) →
χ) |
19 | 3 | nfel1 2499 |
. . . . 5
⊢ Ⅎz A ∈ R |
20 | 5 | nfel1 2499 |
. . . . 5
⊢ Ⅎz B ∈ S |
21 | 6 | nfel1 2499 |
. . . . 5
⊢ Ⅎz C ∈ T |
22 | 19, 20, 21 | nf3an 1827 |
. . . 4
⊢ Ⅎz(A ∈ R ∧ B ∈ S ∧ C ∈ T) |
23 | | vtocl3gaf.3 |
. . . 4
⊢ Ⅎzθ |
24 | 22, 23 | nfim 1813 |
. . 3
⊢ Ⅎz((A ∈ R ∧ B ∈ S ∧ C ∈ T) →
θ) |
25 | | eleq1 2413 |
. . . . 5
⊢ (x = A →
(x ∈
R ↔ A ∈ R)) |
26 | 25 | 3anbi1d 1256 |
. . . 4
⊢ (x = A →
((x ∈
R ∧
y ∈
S ∧
z ∈
T) ↔ (A ∈ R ∧ y ∈ S ∧ z ∈ T))) |
27 | | vtocl3gaf.4 |
. . . 4
⊢ (x = A →
(φ ↔ ψ)) |
28 | 26, 27 | imbi12d 311 |
. . 3
⊢ (x = A →
(((x ∈
R ∧
y ∈
S ∧
z ∈
T) → φ) ↔ ((A ∈ R ∧ y ∈ S ∧ z ∈ T) → ψ))) |
29 | | eleq1 2413 |
. . . . 5
⊢ (y = B →
(y ∈
S ↔ B ∈ S)) |
30 | 29 | 3anbi2d 1257 |
. . . 4
⊢ (y = B →
((A ∈
R ∧
y ∈
S ∧
z ∈
T) ↔ (A ∈ R ∧ B ∈ S ∧ z ∈ T))) |
31 | | vtocl3gaf.5 |
. . . 4
⊢ (y = B →
(ψ ↔ χ)) |
32 | 30, 31 | imbi12d 311 |
. . 3
⊢ (y = B →
(((A ∈
R ∧
y ∈
S ∧
z ∈
T) → ψ) ↔ ((A ∈ R ∧ B ∈ S ∧ z ∈ T) → χ))) |
33 | | eleq1 2413 |
. . . . 5
⊢ (z = C →
(z ∈
T ↔ C ∈ T)) |
34 | 33 | 3anbi3d 1258 |
. . . 4
⊢ (z = C →
((A ∈
R ∧
B ∈
S ∧
z ∈
T) ↔ (A ∈ R ∧ B ∈ S ∧ C ∈ T))) |
35 | | vtocl3gaf.6 |
. . . 4
⊢ (z = C →
(χ ↔ θ)) |
36 | 34, 35 | imbi12d 311 |
. . 3
⊢ (z = C →
(((A ∈
R ∧
B ∈
S ∧
z ∈
T) → χ) ↔ ((A ∈ R ∧ B ∈ S ∧ C ∈ T) → θ))) |
37 | | vtocl3gaf.7 |
. . 3
⊢ ((x ∈ R ∧ y ∈ S ∧ z ∈ T) → φ) |
38 | 1, 2, 3, 4, 5, 6, 12, 18, 24, 28, 32, 36, 37 | vtocl3gf 2917 |
. 2
⊢ ((A ∈ R ∧ B ∈ S ∧ C ∈ T) → ((A
∈ R ∧ B ∈ S ∧ C ∈ T) →
θ)) |
39 | 38 | pm2.43i 43 |
1
⊢ ((A ∈ R ∧ B ∈ S ∧ C ∈ T) → θ) |