Step | Hyp | Ref
| Expression |
1 | | efgval.r |
. 2
⊢ ∼ = (
~FG ‘𝐼) |
2 | | vex 3402 |
. . . . . . . . . . . 12
⊢ 𝑖 ∈ V |
3 | | 2on 8139 |
. . . . . . . . . . . . 13
⊢
2o ∈ On |
4 | 3 | elexi 3417 |
. . . . . . . . . . . 12
⊢
2o ∈ V |
5 | 2, 4 | xpex 7494 |
. . . . . . . . . . 11
⊢ (𝑖 × 2o) ∈
V |
6 | | wrdexg 13965 |
. . . . . . . . . . 11
⊢ ((𝑖 × 2o) ∈ V
→ Word (𝑖 ×
2o) ∈ V) |
7 | | fvi 6744 |
. . . . . . . . . . 11
⊢ (Word
(𝑖 × 2o)
∈ V → ( I ‘Word (𝑖 × 2o)) = Word (𝑖 ×
2o)) |
8 | 5, 6, 7 | mp2b 10 |
. . . . . . . . . 10
⊢ ( I
‘Word (𝑖 ×
2o)) = Word (𝑖
× 2o) |
9 | | xpeq1 5539 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → (𝑖 × 2o) = (𝐼 × 2o)) |
10 | | wrdeq 13977 |
. . . . . . . . . . . 12
⊢ ((𝑖 × 2o) = (𝐼 × 2o) →
Word (𝑖 ×
2o) = Word (𝐼
× 2o)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → Word (𝑖 × 2o) = Word (𝐼 ×
2o)) |
12 | 11 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → ( I ‘Word (𝑖 × 2o)) = ( I ‘Word
(𝐼 ×
2o))) |
13 | 8, 12 | eqtr3id 2787 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → Word (𝑖 × 2o) = ( I ‘Word
(𝐼 ×
2o))) |
14 | | efgval.w |
. . . . . . . . 9
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) |
15 | 13, 14 | eqtr4di 2791 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → Word (𝑖 × 2o) = 𝑊) |
16 | | ereq2 8328 |
. . . . . . . 8
⊢ (Word
(𝑖 × 2o) =
𝑊 → (𝑟 Er Word (𝑖 × 2o) ↔ 𝑟 Er 𝑊)) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → (𝑟 Er Word (𝑖 × 2o) ↔ 𝑟 Er 𝑊)) |
18 | | raleq 3310 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → (∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉) ↔
∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))) |
19 | 18 | ralbidv 3109 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → (∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉) ↔
∀𝑛 ∈
(0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))) |
20 | 15, 19 | raleqbidv 3304 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → (∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈
(0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉) ↔
∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))) |
21 | 17, 20 | anbi12d 634 |
. . . . . 6
⊢ (𝑖 = 𝐼 → ((𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈
(0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) ↔ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)))) |
22 | 21 | abbidv 2802 |
. . . . 5
⊢ (𝑖 = 𝐼 → {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈
(0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} = {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}) |
23 | 22 | inteqd 4841 |
. . . 4
⊢ (𝑖 = 𝐼 → ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈
(0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} = ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}) |
24 | | df-efg 18953 |
. . . 4
⊢
~FG = (𝑖
∈ V ↦ ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈
(0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}) |
25 | 14 | efglem 18960 |
. . . . 5
⊢
∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) |
26 | | intexab 5207 |
. . . . 5
⊢
(∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) ↔ ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ∈
V) |
27 | 25, 26 | mpbi 233 |
. . . 4
⊢ ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ∈
V |
28 | 23, 24, 27 | fvmpt 6775 |
. . 3
⊢ (𝐼 ∈ V → (
~FG ‘𝐼) = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}) |
29 | | fvprc 6666 |
. . . 4
⊢ (¬
𝐼 ∈ V → (
~FG ‘𝐼) = ∅) |
30 | | abn0 4269 |
. . . . . . . 8
⊢ ({𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ≠ ∅
↔ ∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))) |
31 | 25, 30 | mpbir 234 |
. . . . . . 7
⊢ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ≠
∅ |
32 | | intssuni 4858 |
. . . . . . 7
⊢ ({𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ≠ ∅
→ ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ⊆ ∪ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}) |
33 | 31, 32 | ax-mp 5 |
. . . . . 6
⊢ ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ⊆ ∪ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} |
34 | | erssxp 8343 |
. . . . . . . . . . . 12
⊢ (𝑟 Er 𝑊 → 𝑟 ⊆ (𝑊 × 𝑊)) |
35 | 14 | efgrcl 18959 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) |
36 | 35 | simpld 498 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑊 → 𝐼 ∈ V) |
37 | 36 | con3i 157 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝐼 ∈ V → ¬
𝑥 ∈ 𝑊) |
38 | 37 | eq0rdv 4293 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝐼 ∈ V → 𝑊 = ∅) |
39 | 38 | xpeq2d 5555 |
. . . . . . . . . . . . . 14
⊢ (¬
𝐼 ∈ V → (𝑊 × 𝑊) = (𝑊 × ∅)) |
40 | | xp0 5990 |
. . . . . . . . . . . . . 14
⊢ (𝑊 × ∅) =
∅ |
41 | 39, 40 | eqtrdi 2789 |
. . . . . . . . . . . . 13
⊢ (¬
𝐼 ∈ V → (𝑊 × 𝑊) = ∅) |
42 | | ss0b 4286 |
. . . . . . . . . . . . 13
⊢ ((𝑊 × 𝑊) ⊆ ∅ ↔ (𝑊 × 𝑊) = ∅) |
43 | 41, 42 | sylibr 237 |
. . . . . . . . . . . 12
⊢ (¬
𝐼 ∈ V → (𝑊 × 𝑊) ⊆ ∅) |
44 | 34, 43 | sylan9ssr 3891 |
. . . . . . . . . . 11
⊢ ((¬
𝐼 ∈ V ∧ 𝑟 Er 𝑊) → 𝑟 ⊆ ∅) |
45 | 44 | ex 416 |
. . . . . . . . . 10
⊢ (¬
𝐼 ∈ V → (𝑟 Er 𝑊 → 𝑟 ⊆ ∅)) |
46 | 45 | adantrd 495 |
. . . . . . . . 9
⊢ (¬
𝐼 ∈ V → ((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) → 𝑟 ⊆
∅)) |
47 | 46 | alrimiv 1934 |
. . . . . . . 8
⊢ (¬
𝐼 ∈ V →
∀𝑟((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) → 𝑟 ⊆
∅)) |
48 | | sseq1 3902 |
. . . . . . . . 9
⊢ (𝑤 = 𝑟 → (𝑤 ⊆ ∅ ↔ 𝑟 ⊆ ∅)) |
49 | 48 | ralab2 3596 |
. . . . . . . 8
⊢
(∀𝑤 ∈
{𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}𝑤 ⊆ ∅ ↔
∀𝑟((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) → 𝑟 ⊆
∅)) |
50 | 47, 49 | sylibr 237 |
. . . . . . 7
⊢ (¬
𝐼 ∈ V →
∀𝑤 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}𝑤 ⊆
∅) |
51 | | unissb 4830 |
. . . . . . 7
⊢ (∪ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ⊆ ∅
↔ ∀𝑤 ∈
{𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}𝑤 ⊆
∅) |
52 | 50, 51 | sylibr 237 |
. . . . . 6
⊢ (¬
𝐼 ∈ V → ∪ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ⊆
∅) |
53 | 33, 52 | sstrid 3888 |
. . . . 5
⊢ (¬
𝐼 ∈ V → ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ⊆
∅) |
54 | | ss0 4287 |
. . . . 5
⊢ (∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ⊆ ∅
→ ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} =
∅) |
55 | 53, 54 | syl 17 |
. . . 4
⊢ (¬
𝐼 ∈ V → ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} =
∅) |
56 | 29, 55 | eqtr4d 2776 |
. . 3
⊢ (¬
𝐼 ∈ V → (
~FG ‘𝐼) = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}) |
57 | 28, 56 | pm2.61i 185 |
. 2
⊢ (
~FG ‘𝐼) = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} |
58 | 1, 57 | eqtri 2761 |
1
⊢ ∼ =
∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} |