Proof of Theorem efglem
Step | Hyp | Ref
| Expression |
1 | | xpider 7818 |
. 2
⊢ (𝑊 × 𝑊) Er 𝑊 |
2 | | simpll 790 |
. . . . 5
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) → 𝑥 ∈ 𝑊) |
3 | | efgval.w |
. . . . . . . . 9
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
4 | | fviss 6256 |
. . . . . . . . 9
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
5 | 3, 4 | eqsstri 3635 |
. . . . . . . 8
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
6 | 5, 2 | sseldi 3601 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) → 𝑥 ∈ Word (𝐼 ×
2𝑜)) |
7 | | opelxpi 5148 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜) →
〈𝑦, 𝑧〉 ∈ (𝐼 ×
2𝑜)) |
8 | 7 | adantl 482 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) →
〈𝑦, 𝑧〉 ∈ (𝐼 ×
2𝑜)) |
9 | | 2oconcl 7583 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 2𝑜
→ (1𝑜 ∖ 𝑧) ∈
2𝑜) |
10 | | opelxpi 5148 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐼 ∧ (1𝑜 ∖ 𝑧) ∈ 2𝑜)
→ 〈𝑦,
(1𝑜 ∖ 𝑧)〉 ∈ (𝐼 ×
2𝑜)) |
11 | 9, 10 | sylan2 491 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜) →
〈𝑦,
(1𝑜 ∖ 𝑧)〉 ∈ (𝐼 ×
2𝑜)) |
12 | 11 | adantl 482 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) →
〈𝑦,
(1𝑜 ∖ 𝑧)〉 ∈ (𝐼 ×
2𝑜)) |
13 | 8, 12 | s2cld 13616 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) →
〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉 ∈ Word
(𝐼 ×
2𝑜)) |
14 | | splcl 13503 |
. . . . . . 7
⊢ ((𝑥 ∈ Word (𝐼 × 2𝑜) ∧
〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉 ∈ Word
(𝐼 ×
2𝑜)) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
∈ Word (𝐼 ×
2𝑜)) |
15 | 6, 13, 14 | syl2anc 693 |
. . . . . 6
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
∈ Word (𝐼 ×
2𝑜)) |
16 | 3 | efgrcl 18128 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
17 | 16 | simprd 479 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑊 → 𝑊 = Word (𝐼 ×
2𝑜)) |
18 | 17 | ad2antrr 762 |
. . . . . 6
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) → 𝑊 = Word (𝐼 ×
2𝑜)) |
19 | 15, 18 | eleqtrrd 2704 |
. . . . 5
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
∈ 𝑊) |
20 | | brxp 5147 |
. . . . 5
⊢ (𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
↔ (𝑥 ∈ 𝑊 ∧ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
∈ 𝑊)) |
21 | 2, 19, 20 | sylanbrc 698 |
. . . 4
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) → 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)) |
22 | 21 | ralrimivva 2971 |
. . 3
⊢ ((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) → ∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)) |
23 | 22 | rgen2 2975 |
. 2
⊢
∀𝑥 ∈
𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉) |
24 | | fvex 6201 |
. . . . 5
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ∈ V |
25 | 3, 24 | eqeltri 2697 |
. . . 4
⊢ 𝑊 ∈ V |
26 | 25, 25 | xpex 6962 |
. . 3
⊢ (𝑊 × 𝑊) ∈ V |
27 | | ereq1 7749 |
. . . 4
⊢ (𝑟 = (𝑊 × 𝑊) → (𝑟 Er 𝑊 ↔ (𝑊 × 𝑊) Er 𝑊)) |
28 | | breq 4655 |
. . . . . 6
⊢ (𝑟 = (𝑊 × 𝑊) → (𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
↔ 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))) |
29 | 28 | 2ralbidv 2989 |
. . . . 5
⊢ (𝑟 = (𝑊 × 𝑊) → (∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
↔ ∀𝑦 ∈
𝐼 ∀𝑧 ∈ 2𝑜
𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))) |
30 | 29 | 2ralbidv 2989 |
. . . 4
⊢ (𝑟 = (𝑊 × 𝑊) → (∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
↔ ∀𝑥 ∈
𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))) |
31 | 27, 30 | anbi12d 747 |
. . 3
⊢ (𝑟 = (𝑊 × 𝑊) → ((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))
↔ ((𝑊 × 𝑊) Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)))) |
32 | 26, 31 | spcev 3300 |
. 2
⊢ (((𝑊 × 𝑊) Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))
→ ∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))) |
33 | 1, 23, 32 | mp2an 708 |
1
⊢
∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)) |