Step | Hyp | Ref
| Expression |
1 | | isfi 6739 |
. . . . . 6
⊢ (𝑥 ∈ Fin ↔ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦) |
2 | | ensym 6759 |
. . . . . . . 8
⊢ (𝑥 ≈ 𝑦 → 𝑦 ≈ 𝑥) |
3 | | breq1 3992 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ∅ → (𝑦 ≈ 𝑥 ↔ ∅ ≈ 𝑥)) |
4 | 3 | anbi2d 461 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ∅ → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥))) |
5 | 4 | imbi1d 230 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥
∈ 𝐴))) |
6 | 5 | albidv 1817 |
. . . . . . . . . . . 12
⊢ (𝑦 = ∅ → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥
∈ 𝐴))) |
7 | | breq1 3992 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑣 → (𝑦 ≈ 𝑥 ↔ 𝑣 ≈ 𝑥)) |
8 | 7 | anbi2d 461 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑣 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥))) |
9 | 8 | imbi1d 230 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑣 → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
10 | 9 | albidv 1817 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑣 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
11 | | breq1 3992 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = suc 𝑣 → (𝑦 ≈ 𝑥 ↔ suc 𝑣 ≈ 𝑥)) |
12 | 11 | anbi2d 461 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = suc 𝑣 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥))) |
13 | 12 | imbi1d 230 |
. . . . . . . . . . . . 13
⊢ (𝑦 = suc 𝑣 → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
14 | 13 | albidv 1817 |
. . . . . . . . . . . 12
⊢ (𝑦 = suc 𝑣 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
15 | | ensym 6759 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∅
≈ 𝑥 → 𝑥 ≈
∅) |
16 | | en0 6773 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ≈ ∅ ↔ 𝑥 = ∅) |
17 | 15, 16 | sylib 121 |
. . . . . . . . . . . . . . . . . 18
⊢ (∅
≈ 𝑥 → 𝑥 = ∅) |
18 | 17 | anim1i 338 |
. . . . . . . . . . . . . . . . 17
⊢ ((∅
≈ 𝑥 ∧ 𝑥 ≠ ∅) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅)) |
19 | 18 | ancoms 266 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ≠ ∅ ∧ ∅
≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅)) |
20 | 19 | adantll 473 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅)) |
21 | | df-ne 2341 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅) |
22 | | pm3.24 688 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
(𝑥 = ∅ ∧ ¬
𝑥 =
∅) |
23 | 22 | pm2.21i 641 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = ∅ ∧ ¬ 𝑥 = ∅) → ∩ 𝑥
∈ 𝐴) |
24 | 21, 23 | sylan2b 285 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → ∩ 𝑥
∈ 𝐴) |
25 | 20, 24 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥
∈ 𝐴) |
26 | 25 | ax-gen 1442 |
. . . . . . . . . . . . 13
⊢
∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥
∈ 𝐴) |
27 | 26 | a1i 9 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → ∩ 𝑥
∈ 𝐴)) |
28 | | nfv 1521 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑣 ∈ ω ∧
∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴) |
29 | | nfa1 1534 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) |
30 | | simpl 108 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → 𝑥 ⊆ 𝐴) |
31 | | bren 6725 |
. . . . . . . . . . . . . . . . . . 19
⊢ (suc
𝑣 ≈ 𝑥 ↔ ∃𝑓 𝑓:suc 𝑣–1-1-onto→𝑥) |
32 | | ssel 3141 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ⊆ 𝐴 → ((𝑓‘𝑣) ∈ 𝑥 → (𝑓‘𝑣) ∈ 𝐴)) |
33 | | f1of 5442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣⟶𝑥) |
34 | | vex 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑣 ∈ V |
35 | 34 | sucid 4402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑣 ∈ suc 𝑣 |
36 | | ffvelrn 5629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓:suc 𝑣⟶𝑥 ∧ 𝑣 ∈ suc 𝑣) → (𝑓‘𝑣) ∈ 𝑥) |
37 | 33, 35, 36 | sylancl 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓‘𝑣) ∈ 𝑥) |
38 | 32, 37 | impel 278 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) → (𝑓‘𝑣) ∈ 𝐴) |
39 | 38 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑓‘𝑣) ∈ 𝐴) |
40 | 39 | adantlll 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑓‘𝑣) ∈ 𝐴) |
41 | | imaeq2 4949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑣 = ∅ → (𝑓 “ 𝑣) = (𝑓 “ ∅)) |
42 | | ima0 4970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 “ ∅) =
∅ |
43 | 41, 42 | eqtrdi 2219 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = ∅ → (𝑓 “ 𝑣) = ∅) |
44 | | inteq 3834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑓 “ 𝑣) = ∅ → ∩ (𝑓
“ 𝑣) = ∩ ∅) |
45 | | int0 3845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ∩ ∅ = V |
46 | 44, 45 | eqtrdi 2219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑓 “ 𝑣) = ∅ → ∩ (𝑓
“ 𝑣) =
V) |
47 | 46 | ineq1d 3327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑓 “ 𝑣) = ∅ → (∩ (𝑓
“ 𝑣) ∩ (𝑓‘𝑣)) = (V ∩ (𝑓‘𝑣))) |
48 | | ssv 3169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑓‘𝑣) ⊆ V |
49 | | sseqin2 3346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑓‘𝑣) ⊆ V ↔ (V ∩ (𝑓‘𝑣)) = (𝑓‘𝑣)) |
50 | 48, 49 | mpbi 144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (V ∩
(𝑓‘𝑣)) = (𝑓‘𝑣) |
51 | 47, 50 | eqtrdi 2219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓 “ 𝑣) = ∅ → (∩ (𝑓
“ 𝑣) ∩ (𝑓‘𝑣)) = (𝑓‘𝑣)) |
52 | 51 | eleq1d 2239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓 “ 𝑣) = ∅ → ((∩ (𝑓
“ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ (𝑓‘𝑣) ∈ 𝐴)) |
53 | 52 | biimprd 157 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓 “ 𝑣) = ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)) |
54 | 43, 53 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 = ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)) |
55 | 54 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑣 ∈
ω ∧ 𝑥 ⊆
𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ 𝑣 = ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)) |
56 | | f1ofun 5444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → Fun 𝑓) |
57 | 56 | ad3antlr 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑣 ∈
ω ∧ 𝑥 ⊆
𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → Fun 𝑓) |
58 | | elelsuc 4394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (∅
∈ 𝑣 → ∅
∈ suc 𝑣) |
59 | 58 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝑣 ∈
ω ∧ 𝑥 ⊆
𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ suc 𝑣) |
60 | | f1odm 5446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → dom 𝑓 = suc 𝑣) |
61 | 60 | eleq2d 2240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (∅ ∈ dom
𝑓 ↔ ∅ ∈ suc
𝑣)) |
62 | 61 | ad3antlr 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝑣 ∈
ω ∧ 𝑥 ⊆
𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (∅ ∈ dom 𝑓 ↔ ∅ ∈ suc 𝑣)) |
63 | 59, 62 | mpbird 166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑣 ∈
ω ∧ 𝑥 ⊆
𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ dom 𝑓) |
64 | 57, 63 | jca 304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑣 ∈
ω ∧ 𝑥 ⊆
𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (Fun 𝑓 ∧ ∅ ∈ dom 𝑓)) |
65 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑣 ∈
ω ∧ 𝑥 ⊆
𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ 𝑣) |
66 | | funfvima 5727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Fun
𝑓 ∧ ∅ ∈ dom
𝑓) → (∅ ∈
𝑣 → (𝑓‘∅) ∈ (𝑓 “ 𝑣))) |
67 | 64, 65, 66 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑣 ∈
ω ∧ 𝑥 ⊆
𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓‘∅) ∈ (𝑓 “ 𝑣)) |
68 | | ne0i 3421 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓‘∅) ∈ (𝑓 “ 𝑣) → (𝑓 “ 𝑣) ≠ ∅) |
69 | 67, 68 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑣 ∈
ω ∧ 𝑥 ⊆
𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓 “ 𝑣) ≠ ∅) |
70 | | imassrn 4964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑓 “ 𝑣) ⊆ ran 𝑓 |
71 | | dff1o2 5447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 ↔ (𝑓 Fn suc 𝑣 ∧ Fun ◡𝑓 ∧ ran 𝑓 = 𝑥)) |
72 | 71 | simp3bi 1009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ran 𝑓 = 𝑥) |
73 | 70, 72 | sseqtrid 3197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ 𝑣) ⊆ 𝑥) |
74 | | sstr2 3154 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑓 “ 𝑣) ⊆ 𝑥 → (𝑥 ⊆ 𝐴 → (𝑓 “ 𝑣) ⊆ 𝐴)) |
75 | 73, 74 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑥 ⊆ 𝐴 → (𝑓 “ 𝑣) ⊆ 𝐴)) |
76 | 75 | anim1d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅))) |
77 | | f1of1 5441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣–1-1→𝑥) |
78 | | vex 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ 𝑥 ∈ V |
79 | | sssucid 4400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ 𝑣 ⊆ suc 𝑣 |
80 | | f1imaen2g 6771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑓:suc 𝑣–1-1→𝑥 ∧ 𝑥 ∈ V) ∧ (𝑣 ⊆ suc 𝑣 ∧ 𝑣 ∈ V)) → (𝑓 “ 𝑣) ≈ 𝑣) |
81 | 79, 34, 80 | mpanr12 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑓:suc 𝑣–1-1→𝑥 ∧ 𝑥 ∈ V) → (𝑓 “ 𝑣) ≈ 𝑣) |
82 | 77, 78, 81 | sylancl 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ 𝑣) ≈ 𝑣) |
83 | 82 | ensymd 6761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑣 ≈ (𝑓 “ 𝑣)) |
84 | 76, 83 | jctird 315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → (((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)))) |
85 | | vex 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ 𝑓 ∈ V |
86 | 85 | imaex 4966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑓 “ 𝑣) ∈ V |
87 | | sseq1 3170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑥 ⊆ 𝐴 ↔ (𝑓 “ 𝑣) ⊆ 𝐴)) |
88 | | neeq1 2353 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑥 ≠ ∅ ↔ (𝑓 “ 𝑣) ≠ ∅)) |
89 | 87, 88 | anbi12d 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑥 = (𝑓 “ 𝑣) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ↔ ((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅))) |
90 | | breq2 3993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑥 = (𝑓 “ 𝑣) → (𝑣 ≈ 𝑥 ↔ 𝑣 ≈ (𝑓 “ 𝑣))) |
91 | 89, 90 | anbi12d 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 = (𝑓 “ 𝑣) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) ↔ (((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)))) |
92 | | inteq 3834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑥 = (𝑓 “ 𝑣) → ∩ 𝑥 = ∩
(𝑓 “ 𝑣)) |
93 | 92 | eleq1d 2239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 = (𝑓 “ 𝑣) → (∩ 𝑥 ∈ 𝐴 ↔ ∩ (𝑓 “ 𝑣) ∈ 𝐴)) |
94 | 91, 93 | imbi12d 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 = (𝑓 “ 𝑣) → ((((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ↔ ((((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)) → ∩ (𝑓 “ 𝑣) ∈ 𝐴))) |
95 | 86, 94 | spcv 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ((((𝑓 “ 𝑣) ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓 “ 𝑣)) → ∩ (𝑓 “ 𝑣) ∈ 𝐴)) |
96 | 84, 95 | sylan9 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ∩ (𝑓
“ 𝑣) ∈ 𝐴)) |
97 | | ineq1 3321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 = ∩
(𝑓 “ 𝑣) → (𝑧 ∩ 𝑤) = (∩ (𝑓 “ 𝑣) ∩ 𝑤)) |
98 | 97 | eleq1d 2239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 = ∩
(𝑓 “ 𝑣) → ((𝑧 ∩ 𝑤) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑣) ∩ 𝑤) ∈ 𝐴)) |
99 | | ineq2 3322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑤 = (𝑓‘𝑣) → (∩ (𝑓 “ 𝑣) ∩ 𝑤) = (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣))) |
100 | 99 | eleq1d 2239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑤 = (𝑓‘𝑣) → ((∩
(𝑓 “ 𝑣) ∩ 𝑤) ∈ 𝐴 ↔ (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)) |
101 | 98, 100 | rspc2v 2847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((∩ (𝑓
“ 𝑣) ∈ 𝐴 ∧ (𝑓‘𝑣) ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)) |
102 | 101 | ex 114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (∩ (𝑓
“ 𝑣) ∈ 𝐴 → ((𝑓‘𝑣) ∈ 𝐴 → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))) |
103 | 96, 102 | syl6 33 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))) |
104 | 103 | com4r 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑓:suc 𝑣–1-1-onto→𝑥 ∧ ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) → ((𝑥 ⊆ 𝐴 ∧ (𝑓 “ 𝑣) ≠ ∅) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))) |
105 | 104 | exp5c 374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (𝑥 ⊆ 𝐴 → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))))) |
106 | 105 | com14 88 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ⊆ 𝐴 → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)))))) |
107 | 106 | imp43 353 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))) |
108 | 107 | adantlll 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))) |
109 | 108 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑣 ∈
ω ∧ 𝑥 ⊆
𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓 “ 𝑣) ≠ ∅ → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴))) |
110 | 69, 109 | mpd 13 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑣 ∈
ω ∧ 𝑥 ⊆
𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)) |
111 | | 0elnn 4603 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 ∈ ω → (𝑣 = ∅ ∨ ∅ ∈
𝑣)) |
112 | 111 | ad3antrrr 489 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (𝑣 = ∅ ∨ ∅ ∈ 𝑣)) |
113 | 55, 110, 112 | mpjaodan 793 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((𝑓‘𝑣) ∈ 𝐴 → (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴)) |
114 | 40, 113 | mpd 13 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → (∩
(𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴) |
115 | 85, 34 | fvex 5516 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓‘𝑣) ∈ V |
116 | 115 | intunsn 3869 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ∩ ((𝑓
“ 𝑣) ∪ {(𝑓‘𝑣)}) = (∩ (𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) |
117 | | f1ofn 5443 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓 Fn suc 𝑣) |
118 | | fnsnfv 5555 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑓 Fn suc 𝑣 ∧ 𝑣 ∈ suc 𝑣) → {(𝑓‘𝑣)} = (𝑓 “ {𝑣})) |
119 | 117, 35, 118 | sylancl 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → {(𝑓‘𝑣)} = (𝑓 “ {𝑣})) |
120 | 119 | uneq2d 3281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣}))) |
121 | | df-suc 4356 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ suc 𝑣 = (𝑣 ∪ {𝑣}) |
122 | 121 | imaeq2i 4951 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓 “ suc 𝑣) = (𝑓 “ (𝑣 ∪ {𝑣})) |
123 | | imaundi 5023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓 “ (𝑣 ∪ {𝑣})) = ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣})) |
124 | 122, 123 | eqtr2i 2192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓 “ 𝑣) ∪ (𝑓 “ {𝑣})) = (𝑓 “ suc 𝑣) |
125 | 120, 124 | eqtrdi 2219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = (𝑓 “ suc 𝑣)) |
126 | | f1ofo 5449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → 𝑓:suc 𝑣–onto→𝑥) |
127 | | foima 5425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓:suc 𝑣–onto→𝑥 → (𝑓 “ suc 𝑣) = 𝑥) |
128 | 126, 127 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (𝑓 “ suc 𝑣) = 𝑥) |
129 | 125, 128 | eqtrd 2203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((𝑓 “ 𝑣) ∪ {(𝑓‘𝑣)}) = 𝑥) |
130 | 129 | inteqd 3836 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ∩ ((𝑓
“ 𝑣) ∪ {(𝑓‘𝑣)}) = ∩ 𝑥) |
131 | 116, 130 | eqtr3id 2217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → (∩ (𝑓
“ 𝑣) ∩ (𝑓‘𝑣)) = ∩ 𝑥) |
132 | 131 | eleq1d 2239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓:suc 𝑣–1-1-onto→𝑥 → ((∩ (𝑓
“ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴)) |
133 | 132 | ad2antlr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ((∩
(𝑓 “ 𝑣) ∩ (𝑓‘𝑣)) ∈ 𝐴 ↔ ∩ 𝑥 ∈ 𝐴)) |
134 | 114, 133 | mpbid 146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) ∧ 𝑓:suc 𝑣–1-1-onto→𝑥) ∧ (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴)) → ∩ 𝑥 ∈ 𝐴) |
135 | 134 | exp43 370 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) → (𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))) |
136 | 135 | exlimdv 1812 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) → (∃𝑓 𝑓:suc 𝑣–1-1-onto→𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))) |
137 | 31, 136 | syl5bi 151 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 ∈ ω ∧ 𝑥 ⊆ 𝐴) → (suc 𝑣 ≈ 𝑥 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))) |
138 | 137 | expimpd 361 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ suc 𝑣 ≈ 𝑥) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))) |
139 | 30, 138 | sylani 404 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ ω → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))) |
140 | 139 | com24 87 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ ω →
(∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))) |
141 | 140 | imp 123 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ ω ∧
∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
142 | 28, 29, 141 | alrimd 1603 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ ω ∧
∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴) → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
143 | 142 | ex 114 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ ω →
(∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ suc 𝑣 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)))) |
144 | 6, 10, 14, 27, 143 | finds2 4585 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
145 | | sp 1504 |
. . . . . . . . . . 11
⊢
(∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴) → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴)) |
146 | 144, 145 | syl6 33 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑦 ≈ 𝑥) → ∩ 𝑥 ∈ 𝐴))) |
147 | 146 | exp4a 364 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝑦 ≈ 𝑥 → ∩ 𝑥 ∈ 𝐴)))) |
148 | 147 | com24 87 |
. . . . . . . 8
⊢ (𝑦 ∈ ω → (𝑦 ≈ 𝑥 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))) |
149 | 2, 148 | syl5 32 |
. . . . . . 7
⊢ (𝑦 ∈ ω → (𝑥 ≈ 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴)))) |
150 | 149 | rexlimiv 2581 |
. . . . . 6
⊢
(∃𝑦 ∈
ω 𝑥 ≈ 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))) |
151 | 1, 150 | sylbi 120 |
. . . . 5
⊢ (𝑥 ∈ Fin → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴))) |
152 | 151 | com13 80 |
. . . 4
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝑥 ∈ Fin → ∩ 𝑥
∈ 𝐴))) |
153 | 152 | impd 252 |
. . 3
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴)) |
154 | 153 | alrimiv 1867 |
. 2
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴 → ∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴)) |
155 | | ineq1 3321 |
. . . 4
⊢ (𝑥 = 𝑧 → (𝑥 ∩ 𝑦) = (𝑧 ∩ 𝑦)) |
156 | 155 | eleq1d 2239 |
. . 3
⊢ (𝑥 = 𝑧 → ((𝑥 ∩ 𝑦) ∈ 𝐴 ↔ (𝑧 ∩ 𝑦) ∈ 𝐴)) |
157 | | ineq2 3322 |
. . . 4
⊢ (𝑦 = 𝑤 → (𝑧 ∩ 𝑦) = (𝑧 ∩ 𝑤)) |
158 | 157 | eleq1d 2239 |
. . 3
⊢ (𝑦 = 𝑤 → ((𝑧 ∩ 𝑦) ∈ 𝐴 ↔ (𝑧 ∩ 𝑤) ∈ 𝐴)) |
159 | 156, 158 | cbvral2v 2709 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ∩ 𝑤) ∈ 𝐴) |
160 | | df-3an 975 |
. . . 4
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin)) |
161 | 160 | imbi1i 237 |
. . 3
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴) ↔ (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴)) |
162 | 161 | albii 1463 |
. 2
⊢
(∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴) ↔
∀𝑥(((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴)) |
163 | 154, 159,
162 | 3imtr4i 200 |
1
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐴)) |