Step | Hyp | Ref
| Expression |
1 | | df-sfin 4446 |
. . . 4
⊢ ( Sfin (Z,
X) ↔ (Z ∈ Nn ∧ X ∈ Nn ∧ ∃y(℘1y ∈ Z ∧ ℘y ∈ X))) |
2 | | sfineq1 4526 |
. . . . . . 7
⊢ (z = Z → (
Sfin (z, x) ↔
Sfin (Z, x))) |
3 | | eleq1 2413 |
. . . . . . . 8
⊢ (z = Z →
(z ∈
Spfin ↔ Z ∈ Spfin )) |
4 | 3 | imbi2d 307 |
. . . . . . 7
⊢ (z = Z →
((x ∈
Spfin → z ∈ Spfin ) ↔ (x ∈ Spfin → Z ∈ Spfin ))) |
5 | 2, 4 | imbi12d 311 |
. . . . . 6
⊢ (z = Z → ((
Sfin (z, x) →
(x ∈
Spfin → z ∈ Spfin )) ↔ ( Sfin (Z,
x) → (x ∈ Spfin → Z ∈ Spfin )))) |
6 | | sfineq2 4527 |
. . . . . . 7
⊢ (x = X → (
Sfin (Z, x) ↔
Sfin (Z, X))) |
7 | | eleq1 2413 |
. . . . . . . 8
⊢ (x = X →
(x ∈
Spfin ↔ X ∈ Spfin )) |
8 | 7 | imbi1d 308 |
. . . . . . 7
⊢ (x = X →
((x ∈
Spfin → Z ∈ Spfin ) ↔ (X ∈ Spfin → Z ∈ Spfin ))) |
9 | 6, 8 | imbi12d 311 |
. . . . . 6
⊢ (x = X → ((
Sfin (Z, x) →
(x ∈
Spfin → Z ∈ Spfin )) ↔ ( Sfin (Z,
X) → (X ∈ Spfin → Z ∈ Spfin )))) |
10 | | sfineq2 4527 |
. . . . . . . . . . . . . . 15
⊢ (p = x → (
Sfin (q, p) ↔
Sfin (q, x))) |
11 | 10 | imbi1d 308 |
. . . . . . . . . . . . . 14
⊢ (p = x → ((
Sfin (q, p) →
q ∈
a) ↔ ( Sfin (q,
x) → q ∈ a))) |
12 | 11 | albidv 1625 |
. . . . . . . . . . . . 13
⊢ (p = x →
(∀q(
Sfin (q, p) →
q ∈
a) ↔ ∀q( Sfin (q,
x) → q ∈ a))) |
13 | 12 | rspcv 2951 |
. . . . . . . . . . . 12
⊢ (x ∈ a → (∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a) → ∀q( Sfin (q,
x) → q ∈ a))) |
14 | | sfineq1 4526 |
. . . . . . . . . . . . . . 15
⊢ (q = z → (
Sfin (q, x) ↔
Sfin (z, x))) |
15 | | eleq1 2413 |
. . . . . . . . . . . . . . 15
⊢ (q = z →
(q ∈
a ↔ z ∈ a)) |
16 | 14, 15 | imbi12d 311 |
. . . . . . . . . . . . . 14
⊢ (q = z → ((
Sfin (q, x) →
q ∈
a) ↔ ( Sfin (z,
x) → z ∈ a))) |
17 | 16 | spv 1998 |
. . . . . . . . . . . . 13
⊢ (∀q( Sfin (q,
x) → q ∈ a) → ( Sfin (z,
x) → z ∈ a)) |
18 | 17 | com12 27 |
. . . . . . . . . . . 12
⊢ ( Sfin (z,
x) → (∀q( Sfin (q,
x) → q ∈ a) → z
∈ a)) |
19 | 13, 18 | syl9r 67 |
. . . . . . . . . . 11
⊢ ( Sfin (z,
x) → (x ∈ a → (∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a) → z
∈ a))) |
20 | 19 | com23 72 |
. . . . . . . . . 10
⊢ ( Sfin (z,
x) → (∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a) → (x
∈ a
→ z ∈ a))) |
21 | 20 | adantld 453 |
. . . . . . . . 9
⊢ ( Sfin (z,
x) → (( Ncfin V ∈
a ∧ ∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a)) → (x
∈ a
→ z ∈ a))) |
22 | 21 | a2d 23 |
. . . . . . . 8
⊢ ( Sfin (z,
x) → ((( Ncfin V ∈
a ∧ ∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a)) → x
∈ a)
→ (( Ncfin V ∈ a ∧ ∀p ∈ a ∀q( Sfin
(q, p)
→ q ∈ a)) →
z ∈
a))) |
23 | 22 | alimdv 1621 |
. . . . . . 7
⊢ ( Sfin (z,
x) → (∀a(( Ncfin V ∈
a ∧ ∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a)) → x
∈ a)
→ ∀a(( Ncfin V
∈ a ∧ ∀p ∈ a ∀q( Sfin
(q, p)
→ q ∈ a)) →
z ∈
a))) |
24 | | df-spfin 4447 |
. . . . . . . . 9
⊢ Spfin = ∩{a ∣ ( Ncfin V ∈
a ∧ ∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a))} |
25 | 24 | eleq2i 2417 |
. . . . . . . 8
⊢ (x ∈ Spfin ↔ x ∈ ∩{a ∣ ( Ncfin
V ∈ a
∧ ∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a))}) |
26 | | vex 2862 |
. . . . . . . . 9
⊢ x ∈
V |
27 | 26 | elintab 3937 |
. . . . . . . 8
⊢ (x ∈ ∩{a ∣ ( Ncfin
V ∈ a
∧ ∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a))} ↔ ∀a(( Ncfin V ∈
a ∧ ∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a)) → x
∈ a)) |
28 | 25, 27 | bitri 240 |
. . . . . . 7
⊢ (x ∈ Spfin ↔ ∀a(( Ncfin V ∈
a ∧ ∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a)) → x
∈ a)) |
29 | 24 | eleq2i 2417 |
. . . . . . . 8
⊢ (z ∈ Spfin ↔ z ∈ ∩{a ∣ ( Ncfin
V ∈ a
∧ ∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a))}) |
30 | | vex 2862 |
. . . . . . . . 9
⊢ z ∈
V |
31 | 30 | elintab 3937 |
. . . . . . . 8
⊢ (z ∈ ∩{a ∣ ( Ncfin
V ∈ a
∧ ∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a))} ↔ ∀a(( Ncfin V ∈
a ∧ ∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a)) → z
∈ a)) |
32 | 29, 31 | bitri 240 |
. . . . . . 7
⊢ (z ∈ Spfin ↔ ∀a(( Ncfin V ∈
a ∧ ∀p ∈ a ∀q( Sfin (q,
p) → q ∈ a)) → z
∈ a)) |
33 | 23, 28, 32 | 3imtr4g 261 |
. . . . . 6
⊢ ( Sfin (z,
x) → (x ∈ Spfin → z ∈ Spfin )) |
34 | 5, 9, 33 | vtocl2g 2918 |
. . . . 5
⊢ ((Z ∈ Nn ∧ X ∈ Nn ) → ( Sfin (Z,
X) → (X ∈ Spfin → Z ∈ Spfin ))) |
35 | 34 | 3adant3 975 |
. . . 4
⊢ ((Z ∈ Nn ∧ X ∈ Nn ∧ ∃y(℘1y ∈ Z ∧ ℘y ∈ X)) → (
Sfin (Z, X) →
(X ∈
Spfin → Z ∈ Spfin ))) |
36 | 1, 35 | sylbi 187 |
. . 3
⊢ ( Sfin (Z,
X) → ( Sfin (Z,
X) → (X ∈ Spfin → Z ∈ Spfin ))) |
37 | 36 | pm2.43i 43 |
. 2
⊢ ( Sfin (Z,
X) → (X ∈ Spfin → Z ∈ Spfin )) |
38 | 37 | impcom 419 |
1
⊢ ((X ∈ Spfin ∧
Sfin (Z, X)) →
Z ∈ Spfin ) |