| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | efgval.r | . 2
⊢  ∼ = (
~FG ‘𝐼) | 
| 2 |  | vex 3483 | . . . . . . . . . . . 12
⊢ 𝑖 ∈ V | 
| 3 |  | 2on 8521 | . . . . . . . . . . . . 13
⊢
2o ∈ On | 
| 4 | 3 | elexi 3502 | . . . . . . . . . . . 12
⊢
2o ∈ V | 
| 5 | 2, 4 | xpex 7774 | . . . . . . . . . . 11
⊢ (𝑖 × 2o) ∈
V | 
| 6 |  | wrdexg 14563 | . . . . . . . . . . 11
⊢ ((𝑖 × 2o) ∈ V
→ Word (𝑖 ×
2o) ∈ V) | 
| 7 |  | fvi 6984 | . . . . . . . . . . 11
⊢ (Word
(𝑖 × 2o)
∈ V → ( I ‘Word (𝑖 × 2o)) = Word (𝑖 ×
2o)) | 
| 8 | 5, 6, 7 | mp2b 10 | . . . . . . . . . 10
⊢ ( I
‘Word (𝑖 ×
2o)) = Word (𝑖
× 2o) | 
| 9 |  | xpeq1 5698 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → (𝑖 × 2o) = (𝐼 × 2o)) | 
| 10 |  | wrdeq 14575 | . . . . . . . . . . . 12
⊢ ((𝑖 × 2o) = (𝐼 × 2o) →
Word (𝑖 ×
2o) = Word (𝐼
× 2o)) | 
| 11 | 9, 10 | syl 17 | . . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → Word (𝑖 × 2o) = Word (𝐼 ×
2o)) | 
| 12 | 11 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝑖 = 𝐼 → ( I ‘Word (𝑖 × 2o)) = ( I ‘Word
(𝐼 ×
2o))) | 
| 13 | 8, 12 | eqtr3id 2790 | . . . . . . . . 9
⊢ (𝑖 = 𝐼 → Word (𝑖 × 2o) = ( I ‘Word
(𝐼 ×
2o))) | 
| 14 |  | efgval.w | . . . . . . . . 9
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) | 
| 15 | 13, 14 | eqtr4di 2794 | . . . . . . . 8
⊢ (𝑖 = 𝐼 → Word (𝑖 × 2o) = 𝑊) | 
| 16 |  | ereq2 8754 | . . . . . . . 8
⊢ (Word
(𝑖 × 2o) =
𝑊 → (𝑟 Er Word (𝑖 × 2o) ↔ 𝑟 Er 𝑊)) | 
| 17 | 15, 16 | syl 17 | . . . . . . 7
⊢ (𝑖 = 𝐼 → (𝑟 Er Word (𝑖 × 2o) ↔ 𝑟 Er 𝑊)) | 
| 18 |  | raleq 3322 | . . . . . . . . 9
⊢ (𝑖 = 𝐼 → (∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉) ↔
∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))) | 
| 19 | 18 | ralbidv 3177 | . . . . . . . 8
⊢ (𝑖 = 𝐼 → (∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉) ↔
∀𝑛 ∈
(0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))) | 
| 20 | 15, 19 | raleqbidv 3345 | . . . . . . 7
⊢ (𝑖 = 𝐼 → (∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈
(0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉) ↔
∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))) | 
| 21 | 17, 20 | anbi12d 632 | . . . . . 6
⊢ (𝑖 = 𝐼 → ((𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈
(0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) ↔ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)))) | 
| 22 | 21 | abbidv 2807 | . . . . 5
⊢ (𝑖 = 𝐼 → {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈
(0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} = {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}) | 
| 23 | 22 | inteqd 4950 | . . . 4
⊢ (𝑖 = 𝐼 → ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈
(0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} = ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}) | 
| 24 |  | df-efg 19728 | . . . 4
⊢ 
~FG = (𝑖
∈ V ↦ ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈
(0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}) | 
| 25 | 14 | efglem 19735 | . . . . 5
⊢
∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) | 
| 26 |  | intexab 5345 | . . . . 5
⊢
(∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) ↔ ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ∈
V) | 
| 27 | 25, 26 | mpbi 230 | . . . 4
⊢ ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ∈
V | 
| 28 | 23, 24, 27 | fvmpt 7015 | . . 3
⊢ (𝐼 ∈ V → (
~FG ‘𝐼) = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}) | 
| 29 |  | fvprc 6897 | . . . 4
⊢ (¬
𝐼 ∈ V → (
~FG ‘𝐼) = ∅) | 
| 30 |  | abn0 4384 | . . . . . . . 8
⊢ ({𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ≠ ∅
↔ ∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))) | 
| 31 | 25, 30 | mpbir 231 | . . . . . . 7
⊢ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ≠
∅ | 
| 32 |  | intssuni 4969 | . . . . . . 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 8769 | . . . . . . . . . . . 12
⊢ (𝑟 Er 𝑊 → 𝑟 ⊆ (𝑊 × 𝑊)) | 
| 35 | 14 | efgrcl 19734 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) | 
| 36 | 35 | simpld 494 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑊 → 𝐼 ∈ V) | 
| 37 | 36 | con3i 154 | . . . . . . . . . . . . . . . 16
⊢ (¬
𝐼 ∈ V → ¬
𝑥 ∈ 𝑊) | 
| 38 | 37 | eq0rdv 4406 | . . . . . . . . . . . . . . 15
⊢ (¬
𝐼 ∈ V → 𝑊 = ∅) | 
| 39 | 38 | xpeq2d 5714 | . . . . . . . . . . . . . 14
⊢ (¬
𝐼 ∈ V → (𝑊 × 𝑊) = (𝑊 × ∅)) | 
| 40 |  | xp0 6177 | . . . . . . . . . . . . . 14
⊢ (𝑊 × ∅) =
∅ | 
| 41 | 39, 40 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (¬
𝐼 ∈ V → (𝑊 × 𝑊) = ∅) | 
| 42 |  | ss0b 4400 | . . . . . . . . . . . . 13
⊢ ((𝑊 × 𝑊) ⊆ ∅ ↔ (𝑊 × 𝑊) = ∅) | 
| 43 | 41, 42 | sylibr 234 | . . . . . . . . . . . 12
⊢ (¬
𝐼 ∈ V → (𝑊 × 𝑊) ⊆ ∅) | 
| 44 | 34, 43 | sylan9ssr 3997 | . . . . . . . . . . 11
⊢ ((¬
𝐼 ∈ V ∧ 𝑟 Er 𝑊) → 𝑟 ⊆ ∅) | 
| 45 | 44 | ex 412 | . . . . . . . . . 10
⊢ (¬
𝐼 ∈ V → (𝑟 Er 𝑊 → 𝑟 ⊆ ∅)) | 
| 46 | 45 | adantrd 491 | . . . . . . . . 9
⊢ (¬
𝐼 ∈ V → ((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) → 𝑟 ⊆
∅)) | 
| 47 | 46 | alrimiv 1926 | . . . . . . . 8
⊢ (¬
𝐼 ∈ V →
∀𝑟((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) → 𝑟 ⊆
∅)) | 
| 48 |  | sseq1 4008 | . . . . . . . . 9
⊢ (𝑤 = 𝑟 → (𝑤 ⊆ ∅ ↔ 𝑟 ⊆ ∅)) | 
| 49 | 48 | ralab2 3702 | . . . . . . . 8
⊢
(∀𝑤 ∈
{𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}𝑤 ⊆ ∅ ↔
∀𝑟((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) → 𝑟 ⊆
∅)) | 
| 50 | 47, 49 | sylibr 234 | . . . . . . 7
⊢ (¬
𝐼 ∈ V →
∀𝑤 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}𝑤 ⊆
∅) | 
| 51 |  | unissb 4938 | . . . . . . 7
⊢ (∪ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ⊆ ∅
↔ ∀𝑤 ∈
{𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}𝑤 ⊆
∅) | 
| 52 | 50, 51 | sylibr 234 | . . . . . 6
⊢ (¬
𝐼 ∈ V → ∪ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ⊆
∅) | 
| 53 | 33, 52 | sstrid 3994 | . . . . 5
⊢ (¬
𝐼 ∈ V → ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} ⊆
∅) | 
| 54 |  | ss0 4401 | . . . . 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 2779 | . . 3
⊢ (¬
𝐼 ∈ V → (
~FG ‘𝐼) = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))}) | 
| 57 | 28, 56 | pm2.61i 182 | . 2
⊢ (
~FG ‘𝐼) = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} | 
| 58 | 1, 57 | eqtri 2764 | 1
⊢  ∼ =
∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} |