Proof of Theorem efglem
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | xpider 8806 |
. 2
⊢ (𝑊 × 𝑊) Er 𝑊 |
| 2 | | simpll 766 |
. . . . 5
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o)) → 𝑥 ∈ 𝑊) |
| 3 | | efgval.w |
. . . . . . . . 9
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) |
| 4 | | fviss 6975 |
. . . . . . . . 9
⊢ ( I
‘Word (𝐼 ×
2o)) ⊆ Word (𝐼 × 2o) |
| 5 | 3, 4 | eqsstri 4014 |
. . . . . . . 8
⊢ 𝑊 ⊆ Word (𝐼 × 2o) |
| 6 | 5, 2 | sselid 3978 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o)) → 𝑥 ∈ Word (𝐼 × 2o)) |
| 7 | | opelxpi 5715 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o) → ⟨𝑦, 𝑧⟩ ∈ (𝐼 × 2o)) |
| 8 | 7 | adantl 481 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o)) → ⟨𝑦, 𝑧⟩ ∈ (𝐼 × 2o)) |
| 9 | | 2oconcl 8523 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 2o →
(1o ∖ 𝑧)
∈ 2o) |
| 10 | | opelxpi 5715 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐼 ∧ (1o ∖ 𝑧) ∈ 2o) →
⟨𝑦, (1o
∖ 𝑧)⟩ ∈
(𝐼 ×
2o)) |
| 11 | 9, 10 | sylan2 592 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o) → ⟨𝑦, (1o ∖ 𝑧)⟩ ∈ (𝐼 ×
2o)) |
| 12 | 11 | adantl 481 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o)) → ⟨𝑦, (1o ∖ 𝑧)⟩ ∈ (𝐼 ×
2o)) |
| 13 | 8, 12 | s2cld 14854 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o)) →
⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩ ∈ Word (𝐼 ×
2o)) |
| 14 | | splcl 14734 |
. . . . . . 7
⊢ ((𝑥 ∈ Word (𝐼 × 2o) ∧
⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩ ∈ Word (𝐼 × 2o)) →
(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩) ∈ Word
(𝐼 ×
2o)) |
| 15 | 6, 13, 14 | syl2anc 583 |
. . . . . 6
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩) ∈ Word
(𝐼 ×
2o)) |
| 16 | 3 | efgrcl 19669 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) |
| 17 | 16 | simprd 495 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑊 → 𝑊 = Word (𝐼 × 2o)) |
| 18 | 17 | ad2antrr 725 |
. . . . . 6
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o)) → 𝑊 = Word (𝐼 × 2o)) |
| 19 | 15, 18 | eleqtrrd 2832 |
. . . . 5
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩) ∈ 𝑊) |
| 20 | | brxp 5727 |
. . . . 5
⊢ (𝑥(𝑊 × 𝑊)(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩) ↔ (𝑥 ∈ 𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩) ∈ 𝑊)) |
| 21 | 2, 19, 20 | sylanbrc 582 |
. . . 4
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o)) → 𝑥(𝑊 × 𝑊)(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩)) |
| 22 | 21 | ralrimivva 3197 |
. . 3
⊢ ((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥))) → ∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥(𝑊 × 𝑊)(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩)) |
| 23 | 22 | rgen2 3194 |
. 2
⊢
∀𝑥 ∈
𝑊 ∀𝑛 ∈
(0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥(𝑊 × 𝑊)(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩) |
| 24 | 3 | fvexi 6911 |
. . . 4
⊢ 𝑊 ∈ V |
| 25 | 24, 24 | xpex 7755 |
. . 3
⊢ (𝑊 × 𝑊) ∈ V |
| 26 | | ereq1 8731 |
. . . 4
⊢ (𝑟 = (𝑊 × 𝑊) → (𝑟 Er 𝑊 ↔ (𝑊 × 𝑊) Er 𝑊)) |
| 27 | | breq 5150 |
. . . . . 6
⊢ (𝑟 = (𝑊 × 𝑊) → (𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩) ↔ 𝑥(𝑊 × 𝑊)(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))) |
| 28 | 27 | 2ralbidv 3215 |
. . . . 5
⊢ (𝑟 = (𝑊 × 𝑊) → (∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩) ↔
∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥(𝑊 × 𝑊)(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))) |
| 29 | 28 | 2ralbidv 3215 |
. . . 4
⊢ (𝑟 = (𝑊 × 𝑊) → (∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩) ↔
∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥(𝑊 × 𝑊)(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))) |
| 30 | 26, 29 | anbi12d 631 |
. . 3
⊢ (𝑟 = (𝑊 × 𝑊) → ((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩)) ↔ ((𝑊 × 𝑊) Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥(𝑊 × 𝑊)(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩)))) |
| 31 | 25, 30 | spcev 3593 |
. 2
⊢ (((𝑊 × 𝑊) Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥(𝑊 × 𝑊)(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩)) →
∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))) |
| 32 | 1, 23, 31 | mp2an 691 |
1
⊢
∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩)) |
