Step | Hyp | Ref
| Expression |
1 | | efgval.r |
. 2
⊢ ∼ = (
~FG ‘𝐼) |
2 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑖 ∈ V |
3 | | 2on 7455 |
. . . . . . . . . . . . 13
⊢
2𝑜 ∈ On |
4 | 3 | elexi 3186 |
. . . . . . . . . . . 12
⊢
2𝑜 ∈ V |
5 | 2, 4 | xpex 6860 |
. . . . . . . . . . 11
⊢ (𝑖 × 2𝑜)
∈ V |
6 | | wrdexg 13170 |
. . . . . . . . . . 11
⊢ ((𝑖 × 2𝑜)
∈ V → Word (𝑖
× 2𝑜) ∈ V) |
7 | | fvi 6165 |
. . . . . . . . . . 11
⊢ (Word
(𝑖 ×
2𝑜) ∈ V → ( I ‘Word (𝑖 × 2𝑜)) = Word
(𝑖 ×
2𝑜)) |
8 | 5, 6, 7 | mp2b 10 |
. . . . . . . . . 10
⊢ ( I
‘Word (𝑖 ×
2𝑜)) = Word (𝑖 ×
2𝑜) |
9 | | xpeq1 5052 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → (𝑖 × 2𝑜) = (𝐼 ×
2𝑜)) |
10 | | wrdeq 13182 |
. . . . . . . . . . . 12
⊢ ((𝑖 × 2𝑜)
= (𝐼 ×
2𝑜) → Word (𝑖 × 2𝑜) = Word (𝐼 ×
2𝑜)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → Word (𝑖 × 2𝑜) = Word (𝐼 ×
2𝑜)) |
12 | 11 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → ( I ‘Word (𝑖 × 2𝑜)) = ( I
‘Word (𝐼 ×
2𝑜))) |
13 | 8, 12 | syl5eqr 2658 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → Word (𝑖 × 2𝑜) = ( I
‘Word (𝐼 ×
2𝑜))) |
14 | | efgval.w |
. . . . . . . . 9
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
15 | 13, 14 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → Word (𝑖 × 2𝑜) = 𝑊) |
16 | | ereq2 7637 |
. . . . . . . 8
⊢ (Word
(𝑖 ×
2𝑜) = 𝑊
→ (𝑟 Er Word (𝑖 × 2𝑜)
↔ 𝑟 Er 𝑊)) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → (𝑟 Er Word (𝑖 × 2𝑜) ↔ 𝑟 Er 𝑊)) |
18 | | raleq 3115 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → (∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
↔ ∀𝑦 ∈
𝐼 ∀𝑧 ∈ 2𝑜
𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))) |
19 | 18 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → (∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
↔ ∀𝑛 ∈
(0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))) |
20 | 15, 19 | raleqbidv 3129 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → (∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
↔ ∀𝑥 ∈
𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))) |
21 | 17, 20 | anbi12d 743 |
. . . . . 6
⊢ (𝑖 = 𝐼 → ((𝑟 Er Word (𝑖 × 2𝑜) ∧
∀𝑥 ∈ Word
(𝑖 ×
2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))
↔ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)))) |
22 | 21 | abbidv 2728 |
. . . . 5
⊢ (𝑖 = 𝐼 → {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧
∀𝑥 ∈ Word
(𝑖 ×
2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))} =
{𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}) |
23 | 22 | inteqd 4415 |
. . . 4
⊢ (𝑖 = 𝐼 → ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧
∀𝑥 ∈ Word
(𝑖 ×
2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))} =
∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}) |
24 | | df-efg 17945 |
. . . 4
⊢
~FG = (𝑖
∈ V ↦ ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2𝑜) ∧
∀𝑥 ∈ Word
(𝑖 ×
2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}) |
25 | 14 | efglem 17952 |
. . . . 5
⊢
∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)) |
26 | | intexab 4749 |
. . . . 5
⊢
(∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))
↔ ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}
∈ V) |
27 | 25, 26 | mpbi 219 |
. . . 4
⊢ ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}
∈ V |
28 | 23, 24, 27 | fvmpt 6191 |
. . 3
⊢ (𝐼 ∈ V → (
~FG ‘𝐼) = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}) |
29 | | fvprc 6097 |
. . . 4
⊢ (¬
𝐼 ∈ V → (
~FG ‘𝐼) = ∅) |
30 | | abn0 3908 |
. . . . . . . 8
⊢ ({𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}
≠ ∅ ↔ ∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))) |
31 | 25, 30 | mpbir 220 |
. . . . . . 7
⊢ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}
≠ ∅ |
32 | | intssuni 4434 |
. . . . . . 7
⊢ ({𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}
≠ ∅ → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}
⊆ ∪ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}) |
33 | 31, 32 | ax-mp 5 |
. . . . . 6
⊢ ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}
⊆ ∪ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))} |
34 | | erssxp 7652 |
. . . . . . . . . . . 12
⊢ (𝑟 Er 𝑊 → 𝑟 ⊆ (𝑊 × 𝑊)) |
35 | 14 | efgrcl 17951 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
36 | 35 | simpld 474 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑊 → 𝐼 ∈ V) |
37 | 36 | con3i 149 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝐼 ∈ V → ¬
𝑥 ∈ 𝑊) |
38 | 37 | eq0rdv 3931 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝐼 ∈ V → 𝑊 = ∅) |
39 | 38 | xpeq2d 5063 |
. . . . . . . . . . . . . 14
⊢ (¬
𝐼 ∈ V → (𝑊 × 𝑊) = (𝑊 × ∅)) |
40 | | xp0 5471 |
. . . . . . . . . . . . . 14
⊢ (𝑊 × ∅) =
∅ |
41 | 39, 40 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (¬
𝐼 ∈ V → (𝑊 × 𝑊) = ∅) |
42 | | ss0b 3925 |
. . . . . . . . . . . . 13
⊢ ((𝑊 × 𝑊) ⊆ ∅ ↔ (𝑊 × 𝑊) = ∅) |
43 | 41, 42 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (¬
𝐼 ∈ V → (𝑊 × 𝑊) ⊆ ∅) |
44 | 34, 43 | sylan9ssr 3582 |
. . . . . . . . . . 11
⊢ ((¬
𝐼 ∈ V ∧ 𝑟 Er 𝑊) → 𝑟 ⊆ ∅) |
45 | 44 | ex 449 |
. . . . . . . . . 10
⊢ (¬
𝐼 ∈ V → (𝑟 Er 𝑊 → 𝑟 ⊆ ∅)) |
46 | 45 | adantrd 483 |
. . . . . . . . 9
⊢ (¬
𝐼 ∈ V → ((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))
→ 𝑟 ⊆
∅)) |
47 | 46 | alrimiv 1842 |
. . . . . . . 8
⊢ (¬
𝐼 ∈ V →
∀𝑟((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))
→ 𝑟 ⊆
∅)) |
48 | | sseq1 3589 |
. . . . . . . . 9
⊢ (𝑤 = 𝑟 → (𝑤 ⊆ ∅ ↔ 𝑟 ⊆ ∅)) |
49 | 48 | ralab2 3338 |
. . . . . . . 8
⊢
(∀𝑤 ∈
{𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}𝑤 ⊆ ∅ ↔
∀𝑟((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))
→ 𝑟 ⊆
∅)) |
50 | 47, 49 | sylibr 223 |
. . . . . . 7
⊢ (¬
𝐼 ∈ V →
∀𝑤 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}𝑤 ⊆
∅) |
51 | | unissb 4405 |
. . . . . . 7
⊢ (∪ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}
⊆ ∅ ↔ ∀𝑤 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}𝑤 ⊆
∅) |
52 | 50, 51 | sylibr 223 |
. . . . . 6
⊢ (¬
𝐼 ∈ V → ∪ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}
⊆ ∅) |
53 | 33, 52 | syl5ss 3579 |
. . . . 5
⊢ (¬
𝐼 ∈ V → ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}
⊆ ∅) |
54 | | ss0 3926 |
. . . . 5
⊢ (∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}
⊆ ∅ → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))} =
∅) |
55 | 53, 54 | syl 17 |
. . . 4
⊢ (¬
𝐼 ∈ V → ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))} =
∅) |
56 | 29, 55 | eqtr4d 2647 |
. . 3
⊢ (¬
𝐼 ∈ V → (
~FG ‘𝐼) = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}) |
57 | 28, 56 | pm2.61i 175 |
. 2
⊢ (
~FG ‘𝐼) = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))} |
58 | 1, 57 | eqtri 2632 |
1
⊢ ∼ =
∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))} |