Proof of Theorem fiint
| Step | Hyp | Ref
| Expression |
| 1 | | breq1 2617 |
. . . . . . . . . . . . . . 15
⊢ (y =
∅ → (y ≈ x ↔ ∅ ≈ x)) |
| 2 | 1 | anbi2d 615 |
. . . . . . . . . . . . . 14
⊢ (y =
∅ → (((x ⊆ A ⋀ x ≠
∅) ⋀ y ≈ x) ↔ ((x
⊆ A ⋀ x ≠ ∅) ⋀ ∅ ≈ x))) |
| 3 | 2 | imbi1d 612 |
. . . . . . . . . . . . 13
⊢ (y =
∅ → ((((x ⊆ A ⋀ x ≠
∅) ⋀ y ≈ x) → ∩x ∈ A)
↔ (((x ⊆ A ⋀ x ≠
∅) ⋀ ∅ ≈ x) →
∩x ∈
A))) |
| 4 | 3 | albidv 1276 |
. . . . . . . . . . . 12
⊢ (y =
∅ → (∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ y ≈ x)
→ ∩x ∈
A) ↔ ∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ ∅ ≈ x) → ∩x ∈ A))) |
| 5 | | breq1 2617 |
. . . . . . . . . . . . . . 15
⊢ (y =
v → (y ≈ x
↔ v ≈ x)) |
| 6 | 5 | anbi2d 615 |
. . . . . . . . . . . . . 14
⊢ (y =
v → (((x ⊆ A
⋀ x ≠ ∅) ⋀ y ≈ x)
↔ ((x ⊆ A ⋀ x ≠
∅) ⋀ v ≈ x))) |
| 7 | 6 | imbi1d 612 |
. . . . . . . . . . . . 13
⊢ (y =
v → ((((x ⊆ A
⋀ x ≠ ∅) ⋀ y ≈ x)
→ ∩x ∈
A) ↔ (((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A))) |
| 8 | 7 | albidv 1276 |
. . . . . . . . . . . 12
⊢ (y =
v → (∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ y ≈ x)
→ ∩x ∈
A) ↔ ∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A))) |
| 9 | | breq1 2617 |
. . . . . . . . . . . . . . 15
⊢ (y =
suc v → (y ≈ x
↔ suc v ≈ x)) |
| 10 | 9 | anbi2d 615 |
. . . . . . . . . . . . . 14
⊢ (y =
suc v → (((x ⊆ A
⋀ x ≠ ∅) ⋀ y ≈ x)
↔ ((x ⊆ A ⋀ x ≠
∅) ⋀ suc v ≈ x))) |
| 11 | 10 | imbi1d 612 |
. . . . . . . . . . . . 13
⊢ (y =
suc v → ((((x ⊆ A
⋀ x ≠ ∅) ⋀ y ≈ x)
→ ∩x ∈
A) ↔ (((x ⊆ A
⋀ x ≠ ∅) ⋀ suc
v ≈ x) → ∩x ∈ A))) |
| 12 | 11 | albidv 1276 |
. . . . . . . . . . . 12
⊢ (y =
suc v → (∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ y ≈ x)
→ ∩x ∈
A) ↔ ∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ suc v ≈ x)
→ ∩x ∈
A))) |
| 13 | | visset 1809 |
. . . . . . . . . . . . . . . . . . . 20
⊢ x
∈ V |
| 14 | 13 | ensym 4399 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∅ ≈ x → x
≈ ∅) |
| 15 | | en0 4410 |
. . . . . . . . . . . . . . . . . . 19
⊢ (x
≈ ∅ ↔ x =
∅) |
| 16 | 14, 15 | sylib 198 |
. . . . . . . . . . . . . . . . . 18
⊢ (∅ ≈ x → x =
∅) |
| 17 | 16 | anim1i 334 |
. . . . . . . . . . . . . . . . 17
⊢ ((∅ ≈ x ⋀ x ≠
∅) → (x = ∅ ⋀
x ≠ ∅)) |
| 18 | 17 | ancoms 436 |
. . . . . . . . . . . . . . . 16
⊢ ((x
≠ ∅ ⋀ ∅ ≈ x)
→ (x = ∅ ⋀ x ≠ ∅)) |
| 19 | 18 | adantll 392 |
. . . . . . . . . . . . . . 15
⊢ (((x
⊆ A ⋀ x ≠ ∅) ⋀ ∅ ≈ x) → (x =
∅ ⋀ x ≠ ∅)) |
| 20 | | pm3.24 657 |
. . . . . . . . . . . . . . . . 17
⊢ ¬ (x = ∅ ⋀ ¬ x = ∅) |
| 21 | 20 | pm2.21i 77 |
. . . . . . . . . . . . . . . 16
⊢ ((x =
∅ ⋀ ¬ x = ∅) →
∩x ∈
A) |
| 22 | | df-ne 1584 |
. . . . . . . . . . . . . . . 16
⊢ (x
≠ ∅ ↔ ¬ x =
∅) |
| 23 | 21, 22 | sylan2b 452 |
. . . . . . . . . . . . . . 15
⊢ ((x =
∅ ⋀ x ≠ ∅) →
∩x ∈
A) |
| 24 | 19, 23 | syl 10 |
. . . . . . . . . . . . . 14
⊢ (((x
⊆ A ⋀ x ≠ ∅) ⋀ ∅ ≈ x) → ∩x ∈ A) |
| 25 | 24 | ax-gen 961 |
. . . . . . . . . . . . 13
⊢ ∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ ∅ ≈ x) → ∩x ∈ A) |
| 26 | 25 | a1i 8 |
. . . . . . . . . . . 12
⊢ (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ ∅ ≈ x) → ∩x ∈ A)) |
| 27 | | ax-17 969 |
. . . . . . . . . . . . . 14
⊢ (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ∀x∀z
∈ A ∀w ∈ A
(z ∩ w) ∈ A) |
| 28 | | hba1 1001 |
. . . . . . . . . . . . . 14
⊢ (∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) → ∀x∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A)) |
| 29 | | ssel 2059 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (x
⊆ A → ((f ‘v)
∈ x → (f ‘v)
∈ A)) |
| 30 | | f1ofo 3686 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (f:suc
v–1-1-onto→x →
f:suc v–onto→x) |
| 31 | | fof 3663 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (f:suc
v–onto→x →
f:suc v–→x) |
| 32 | | visset 1809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ v
∈ V |
| 33 | 32 | sucid 3046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ v
∈ suc v |
| 34 | | ffvelrn 3805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((f:suc v–→x
⋀ v ∈ suc v) → (f
‘v) ∈ x) |
| 35 | 33, 34 | mpan2 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (f:suc
v–→x → (f
‘v) ∈ x) |
| 36 | 30, 31, 35 | 3syl 20 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (f:suc
v–1-1-onto→x →
(f ‘v) ∈ x) |
| 37 | 29, 36 | syl5 21 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (x
⊆ A → (f:suc v–1-1-onto→x →
(f ‘v) ∈ A)) |
| 38 | 37 | imp 350 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((x
⊆ A ⋀ f:suc v–1-1-onto→x) →
(f ‘v) ∈ A) |
| 39 | 38 | adantr 389 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((x
⊆ A ⋀ f:suc v–1-1-onto→x) ⋀
(∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) ⋀ ∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A)) → (f
‘v) ∈ A) |
| 40 | | imassrn 3407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (f
“ v) ⊆ ran f |
| 41 | | f1o2 3684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (f:suc
v–1-1-onto→x ↔
(f Fn suc v ⋀ Fun ◡f
⋀ ran f = x)) |
| 42 | | 3simp3 789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((f Fn
suc v ⋀ Fun ◡f
⋀ ran f = x) → ran f
= x) |
| 43 | 41, 42 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (f:suc
v–1-1-onto→x →
ran f = x) |
| 44 | 43 | sseq2d 2085 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (f:suc
v–1-1-onto→x →
((f “ v) ⊆ ran f
↔ (f “ v) ⊆ x)) |
| 45 | 40, 44 | mpbii 193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (f:suc
v–1-1-onto→x →
(f “ v) ⊆ x) |
| 46 | | sstr2 2067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((f
“ v) ⊆ x → (x
⊆ A → (f “ v)
⊆ A)) |
| 47 | 45, 46 | syl 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (f:suc
v–1-1-onto→x →
(x ⊆ A → (f
“ v) ⊆ A)) |
| 48 | 47 | anim1d 559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (f:suc
v–1-1-onto→x →
((x ⊆ A ⋀ (f
“ v) ≠ ∅) → ((f “ v)
⊆ A ⋀ (f “ v)
≠ ∅))) |
| 49 | | f1of1 3679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (f:suc
v–1-1-onto→x →
f:suc v–1-1→x) |
| 50 | | sssucid 3042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ v
⊆ suc v |
| 51 | | f1ores 3694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((f:suc v–1-1→x ⋀
v ⊆ suc v) → (f
↾ v):v–1-1-onto→(f “
v)) |
| 52 | 50, 51 | mpan2 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (f:suc
v–1-1→x →
(f ↾ v):v–1-1-onto→(f “
v)) |
| 53 | 32 | f1oen 4385 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((f
↾ v):v–1-1-onto→(f “
v) → v ≈ (f
“ v)) |
| 54 | 49, 52, 53 | 3syl 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (f:suc
v–1-1-onto→x →
v ≈ (f “ v)) |
| 55 | 48, 54 | jctird 601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (f:suc
v–1-1-onto→x →
((x ⊆ A ⋀ (f
“ v) ≠ ∅) → (((f “ v)
⊆ A ⋀ (f “ v)
≠ ∅) ⋀ v ≈ (f “ v)))) |
| 56 | | visset 1809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ f
∈ V |
| 57 | | imaexg 3408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (f
∈ V → (f “ v) ∈ V) |
| 58 | 56, 57 | ax-mp 7 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (f
“ v) ∈ V |
| 59 | | sseq1 2078 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (x =
(f “ v) → (x
⊆ A ↔ (f “ v)
⊆ A)) |
| 60 | | neeq1 1587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (x =
(f “ v) → (x
≠ ∅ ↔ (f “ v) ≠ ∅)) |
| 61 | 59, 60 | anbi12d 627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (x =
(f “ v) → ((x
⊆ A ⋀ x ≠ ∅) ↔ ((f “ v)
⊆ A ⋀ (f “ v)
≠ ∅))) |
| 62 | | breq2 2618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (x =
(f “ v) → (v
≈ x ↔ v ≈ (f
“ v))) |
| 63 | 61, 62 | anbi12d 627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (x =
(f “ v) → (((x
⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x)
↔ (((f “ v) ⊆ A
⋀ (f “ v) ≠ ∅) ⋀ v ≈ (f
“ v)))) |
| 64 | | inteq 2531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (x =
(f “ v) → ∩x = ∩(f “ v)) |
| 65 | 64 | eleq1d 1537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (x =
(f “ v) → (∩x ∈ A
↔ ∩(f
“ v) ∈ A)) |
| 66 | 63, 65 | imbi12d 625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (x =
(f “ v) → ((((x
⊆ A ⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) ↔ ((((f “ v)
⊆ A ⋀ (f “ v)
≠ ∅) ⋀ v ≈ (f “ v))
→ ∩(f
“ v) ∈ A))) |
| 67 | 58, 66 | cla4v 1864 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) → ((((f “ v)
⊆ A ⋀ (f “ v)
≠ ∅) ⋀ v ≈ (f “ v))
→ ∩(f
“ v) ∈ A)) |
| 68 | 55, 67 | sylan9 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((f:suc v–1-1-onto→x ⋀
∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A)) → ((x ⊆ A
⋀ (f “ v) ≠ ∅) → ∩(f “ v) ∈ A)) |
| 69 | | ineq1 2206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (z =
∩(f “
v) → (z ∩ w) =
(∩(f “
v) ∩ w)) |
| 70 | 69 | eleq1d 1537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (z =
∩(f “
v) → ((z ∩ w)
∈ A ↔ (∩(f “ v) ∩ w)
∈ A)) |
| 71 | | ineq2 2207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (w =
(f ‘v) → (∩(f “ v)
∩ w) = (∩(f “ v) ∩ (f
‘v))) |
| 72 | 71 | eleq1d 1537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (w =
(f ‘v) → ((∩(f “ v)
∩ w) ∈ A ↔ (∩(f “ v)
∩ (f ‘v)) ∈ A)) |
| 73 | 70, 72 | rcla42v 1876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((∩(f “ v)
∈ A ⋀ (f ‘v)
∈ A) → (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → (∩(f “ v)
∩ (f ‘v)) ∈ A)) |
| 74 | 73 | ex 373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (∩(f “ v)
∈ A → ((f ‘v)
∈ A → (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → (∩(f “ v)
∩ (f ‘v)) ∈ A))) |
| 75 | 68, 74 | syl6 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((f:suc v–1-1-onto→x ⋀
∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A)) → ((x ⊆ A
⋀ (f “ v) ≠ ∅) → ((f ‘v)
∈ A → (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → (∩(f “ v)
∩ (f ‘v)) ∈ A)))) |
| 76 | 75 | com4r 41 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ((f:suc
v–1-1-onto→x ⋀
∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A)) → ((x ⊆ A
⋀ (f “ v) ≠ ∅) → ((f ‘v)
∈ A → (∩(f “ v) ∩ (f
‘v)) ∈ A)))) |
| 77 | 76 | exp4a 378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ((f:suc
v–1-1-onto→x ⋀
∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A)) → (x ⊆ A
→ ((f “ v) ≠ ∅ → ((f ‘v)
∈ A → (∩(f “ v) ∩ (f
‘v)) ∈ A))))) |
| 78 | 77 | exp3a 375 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → (f:suc
v–1-1-onto→x →
(∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) → (x ⊆ A
→ ((f “ v) ≠ ∅ → ((f ‘v)
∈ A → (∩(f “ v) ∩ (f
‘v)) ∈ A)))))) |
| 79 | 78 | com14 38 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (x
⊆ A → (f:suc v–1-1-onto→x →
(∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) → (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ((f
“ v) ≠ ∅ → ((f ‘v)
∈ A → (∩(f “ v) ∩ (f
‘v)) ∈ A)))))) |
| 80 | 79 | imp43 370 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((x
⊆ A ⋀ f:suc v–1-1-onto→x) ⋀
(∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) ⋀ ∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A)) → ((f
“ v) ≠ ∅ → ((f ‘v)
∈ A → (∩(f “ v) ∩ (f
‘v)) ∈ A))) |
| 81 | | df-ne 1584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((f
“ v) ≠ ∅ ↔ ¬
(f “ v) = ∅) |
| 82 | 80, 81 | syl5ibr 207 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((x
⊆ A ⋀ f:suc v–1-1-onto→x) ⋀
(∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) ⋀ ∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A)) → (¬ (f “ v) =
∅ → ((f ‘v) ∈ A
→ (∩(f
“ v) ∩ (f ‘v))
∈ A))) |
| 83 | | inteq 2531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((f
“ v) = ∅ → ∩(f “ v) = ∩∅) |
| 84 | | int0 2542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ∩∅ =
V |
| 85 | 83, 84 | syl6eq 1520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((f
“ v) = ∅ → ∩(f “ v) = V) |
| 86 | 85 | ineq1d 2212 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((f
“ v) = ∅ → (∩(f “ v) ∩ (f
‘v)) = (V ∩ (f ‘v))) |
| 87 | | ssv 2077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (f
‘v) ⊆ V |
| 88 | | sseqin2 2225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((f
‘v) ⊆ V ↔ (V
∩ (f ‘v)) = (f
‘v)) |
| 89 | 87, 88 | mpbi 189 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (V ∩ (f ‘v)) =
(f ‘v) |
| 90 | 86, 89 | syl6eq 1520 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((f
“ v) = ∅ → (∩(f “ v) ∩ (f
‘v)) = (f ‘v)) |
| 91 | 90 | eleq1d 1537 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((f
“ v) = ∅ → ((∩(f “ v) ∩ (f
‘v)) ∈ A ↔ (f
‘v) ∈ A)) |
| 92 | 91 | biimprd 154 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((f
“ v) = ∅ → ((f ‘v)
∈ A → (∩(f “ v) ∩ (f
‘v)) ∈ A)) |
| 93 | 82, 92 | pm2.61d2 129 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((x
⊆ A ⋀ f:suc v–1-1-onto→x) ⋀
(∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) ⋀ ∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A)) → ((f
‘v) ∈ A → (∩(f “ v)
∩ (f ‘v)) ∈ A)) |
| 94 | 39, 93 | mpd 26 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((x
⊆ A ⋀ f:suc v–1-1-onto→x) ⋀
(∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) ⋀ ∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A)) → (∩(f “ v)
∩ (f ‘v)) ∈ A) |
| 95 | | f1ofn 3681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (f:suc
v–1-1-onto→x →
f Fn suc v) |
| 96 | | fnsnfv 3758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((f Fn
suc v ⋀ v ∈ suc v)
→ {(f ‘v)} = (f “
{v})) |
| 97 | 33, 96 | mpan2 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (f Fn
suc v → {(f ‘v)} =
(f “ {v})) |
| 98 | 95, 97 | syl 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (f:suc
v–1-1-onto→x →
{(f ‘v)} = (f “
{v})) |
| 99 | 98 | uneq2d 2180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (f:suc
v–1-1-onto→x →
((f “ v) ∪ {(f
‘v)}) = ((f “ v)
∪ (f “ {v}))) |
| 100 | | df-suc 2949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ suc v
= (v ∪ {v}) |
| 101 | | imaeq2 3394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (suc v
= (v ∪ {v}) → (f
“ suc v) = (f “ (v
∪ {v}))) |
| 102 | 100, 101 | ax-mp 7 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (f
“ suc v) = (f “ (v
∪ {v})) |
| 103 | | imaun 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (f
“ (v ∪ {v})) = ((f
“ v) ∪ (f “ {v})) |
| 104 | 102, 103 | eqtr2 1493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((f
“ v) ∪ (f “ {v}))
= (f “ suc v) |
| 105 | 99, 104 | syl6eq 1520 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (f:suc
v–1-1-onto→x →
((f “ v) ∪ {(f
‘v)}) = (f “ suc v)) |
| 106 | | foima 3667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (f:suc
v–onto→x →
(f “ suc v) = x) |
| 107 | 30, 106 | syl 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (f:suc
v–1-1-onto→x →
(f “ suc v) = x) |
| 108 | 105, 107 | eqtrd 1504 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (f:suc
v–1-1-onto→x →
((f “ v) ∪ {(f
‘v)}) = x) |
| 109 | 108 | inteqd 2533 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (f:suc
v–1-1-onto→x →
∩((f “
v) ∪ {(f ‘v)}) =
∩x) |
| 110 | | fvex 3723 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (f
‘v) ∈ V |
| 111 | 110 | intunsn 2560 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∩((f “ v)
∪ {(f ‘v)}) = (∩(f “ v)
∩ (f ‘v)) |
| 112 | 109, 111 | syl5eqr 1518 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (f:suc
v–1-1-onto→x →
(∩(f “
v) ∩ (f ‘v)) =
∩x) |
| 113 | 112 | eleq1d 1537 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (f:suc
v–1-1-onto→x →
((∩(f “
v) ∩ (f ‘v))
∈ A ↔ ∩x ∈ A)) |
| 114 | 113 | ad2antlr 405 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((x
⊆ A ⋀ f:suc v–1-1-onto→x) ⋀
(∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) ⋀ ∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A)) → ((∩(f “ v)
∩ (f ‘v)) ∈ A
↔ ∩x ∈
A)) |
| 115 | 94, 114 | mpbid 195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((x
⊆ A ⋀ f:suc v–1-1-onto→x) ⋀
(∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) ⋀ ∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A)) → ∩x ∈ A) |
| 116 | 115 | exp43 384 |
. . . . . . . . . . . . . . . . . . 19
⊢ (x
⊆ A → (f:suc v–1-1-onto→x →
(∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) → (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ∩x ∈ A)))) |
| 117 | 116 | 19.23adv 1212 |
. . . . . . . . . . . . . . . . . 18
⊢ (x
⊆ A → (∃f f:suc v–1-1-onto→x →
(∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) → (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ∩x ∈ A)))) |
| 118 | 13 | bren 4365 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc v
≈ x ↔ ∃f f:suc v–1-1-onto→x) |
| 119 | 117, 118 | syl5ib 206 |
. . . . . . . . . . . . . . . . 17
⊢ (x
⊆ A → (suc v ≈ x
→ (∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) → (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ∩x ∈ A)))) |
| 120 | 119 | imp 350 |
. . . . . . . . . . . . . . . 16
⊢ ((x
⊆ A ⋀ suc v ≈ x)
→ (∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) → (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ∩x ∈ A))) |
| 121 | 120 | adantlr 393 |
. . . . . . . . . . . . . . 15
⊢ (((x
⊆ A ⋀ x ≠ ∅) ⋀ suc v ≈ x)
→ (∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) → (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ∩x ∈ A))) |
| 122 | 121 | com13 33 |
. . . . . . . . . . . . . 14
⊢ (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → (∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) → (((x ⊆ A
⋀ x ≠ ∅) ⋀ suc
v ≈ x) → ∩x ∈ A))) |
| 123 | 27, 28, 122 | 19.21ad 1057 |
. . . . . . . . . . . . 13
⊢ (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → (∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) → ∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ suc v ≈ x)
→ ∩x ∈
A))) |
| 124 | 123 | a1i 8 |
. . . . . . . . . . . 12
⊢ (v
∈ ω → (∀z ∈
A ∀w ∈ A
(z ∩ w) ∈ A
→ (∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ v ≈ x)
→ ∩x ∈
A) → ∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ suc v ≈ x)
→ ∩x ∈
A)))) |
| 125 | 4, 8, 12, 26, 124 | finds2 3153 |
. . . . . . . . . . 11
⊢ (y
∈ ω → (∀z ∈
A ∀w ∈ A
(z ∩ w) ∈ A
→ ∀x(((x ⊆ A
⋀ x ≠ ∅) ⋀ y ≈ x)
→ ∩x ∈
A))) |
| 126 | | ax-4 971 |
. . . . . . . . . . 11
⊢ (∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ y ≈ x)
→ ∩x ∈
A) → (((x ⊆ A
⋀ x ≠ ∅) ⋀ y ≈ x)
→ ∩x ∈
A)) |
| 127 | 125, 126 | syl6 22 |
. . . . . . . . . 10
⊢ (y
∈ ω → (∀z ∈
A ∀w ∈ A
(z ∩ w) ∈ A
→ (((x ⊆ A ⋀ x ≠
∅) ⋀ y ≈ x) → ∩x ∈ A))) |
| 128 | 127 | exp4a 378 |
. . . . . . . . 9
⊢ (y
∈ ω → (∀z ∈
A ∀w ∈ A
(z ∩ w) ∈ A
→ ((x ⊆ A ⋀ x ≠
∅) → (y ≈ x → ∩x ∈ A)))) |
| 129 | 128 | com24 37 |
. . . . . . . 8
⊢ (y
∈ ω → (y ≈ x → ((x
⊆ A ⋀ x ≠ ∅) → (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ∩x ∈ A)))) |
| 130 | | visset 1809 |
. . . . . . . . 9
⊢ y
∈ V |
| 131 | 130 | ensym 4399 |
. . . . . . . 8
⊢ (x
≈ y → y ≈ x) |
| 132 | 129, 131 | syl5 21 |
. . . . . . 7
⊢ (y
∈ ω → (x ≈ y → ((x
⊆ A ⋀ x ≠ ∅) → (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ∩x ∈ A)))) |
| 133 | 132 | r19.23aiv 1740 |
. . . . . 6
⊢ (∃y ∈ ω x ≈ y
→ ((x ⊆ A ⋀ x ≠
∅) → (∀z ∈ A ∀w
∈ A (z ∩ w)
∈ A → ∩x ∈ A))) |
| 134 | 133 | com13 33 |
. . . . 5
⊢ (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ((x
⊆ A ⋀ x ≠ ∅) → (∃y ∈ ω x ≈ y
→ ∩x ∈
A))) |
| 135 | 134 | imp3a 361 |
. . . 4
⊢ (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → (((x
⊆ A ⋀ x ≠ ∅) ⋀ ∃y ∈ ω x ≈ y)
→ ∩x ∈
A)) |
| 136 | 135 | 19.21aiv 1284 |
. . 3
⊢ (∀z ∈ A
∀w ∈ A (z ∩
w) ∈ A → ∀x(((x ⊆
A ⋀ x ≠ ∅) ⋀ ∃y ∈ ω x ≈ y)
→ ∩x ∈
A)) |
| 137 | | zfpair2 2775 |
. . . . . 6
⊢ {z,
w} ∈ V |
| 138 | | sseq1 2078 |
. . . . . . . . 9
⊢ (x =
{z, w}
→ (x ⊆ A ↔ {z,
w} ⊆ A)) |
| 139 | | neeq1 1587 |
. . . . . . . . 9
⊢ (x =
{z, w}
→ (x ≠ ∅ ↔ {z, w} ≠
∅)) |
| 140 | 138, 139 | anbi12d 627 |
. . . . . . . 8
⊢ (x =
{z, w}
→ ((x ⊆ A ⋀ x ≠
∅) ↔ ({z, w} ⊆ A
⋀ {z, w} ≠ ∅))) |
| 141 | | breq1 2617 |
. . . . . . . . 9
⊢ (x =
{z, w}
→ (x ≈ y ↔ {z,
w} ≈ y)) |
| 142 | 141 | rexbidv 1661 |
. . . . . . . 8
⊢ (x =
{z, w}
→ (∃y ∈ ω x ≈ y
↔ ∃y ∈ ω {z, w} ≈
y)) |
| 143 | 140, 142 | anbi12d 627 |
. . . . . . 7
⊢ (x =
{z, w}
→ (((x ⊆ A ⋀ x ≠
∅) ⋀ ∃y ∈ ω
x ≈ y) ↔ (({z,
w} ⊆ A ⋀ {z,
w} ≠ ∅) ⋀ ∃y ∈ ω {z, w} ≈
y))) |
| 144 | | inteq 2531 |
. . . . . . . 8
⊢ (x =
{z, w}
→ ∩x =
∩{z, w}) |
| 145 | 144 | eleq1d 1537 |
. . . . . . 7
⊢ (x =
{z, w}
→ (∩x
∈ A ↔ ∩{z, w} ∈ A)) |
| 146 | 143, 145 | imbi12d 625 |
. . . . . 6
⊢ (x =
{z, w}
→ ((((x ⊆ A ⋀ x ≠
∅) ⋀ ∃y ∈ ω
x ≈ y) → ∩x ∈ A)
↔ ((({z, w} ⊆ A
|