Proof of Theorem efglem
Step | Hyp | Ref
| Expression |
1 | | xpider 7705 |
. 2
⊢ (𝑊 × 𝑊) Er 𝑊 |
2 | | simpll 786 |
. . . . 5
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) → 𝑥 ∈ 𝑊) |
3 | | efgval.w |
. . . . . . . . 9
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
4 | | fviss 6166 |
. . . . . . . . 9
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
5 | 3, 4 | eqsstri 3598 |
. . . . . . . 8
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
6 | 5, 2 | sseldi 3566 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) → 𝑥 ∈ Word (𝐼 ×
2𝑜)) |
7 | | opelxpi 5072 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜) →
〈𝑦, 𝑧〉 ∈ (𝐼 ×
2𝑜)) |
8 | 7 | adantl 481 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) →
〈𝑦, 𝑧〉 ∈ (𝐼 ×
2𝑜)) |
9 | | 2oconcl 7470 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 2𝑜
→ (1𝑜 ∖ 𝑧) ∈
2𝑜) |
10 | | opelxpi 5072 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐼 ∧ (1𝑜 ∖ 𝑧) ∈ 2𝑜)
→ 〈𝑦,
(1𝑜 ∖ 𝑧)〉 ∈ (𝐼 ×
2𝑜)) |
11 | 9, 10 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜) →
〈𝑦,
(1𝑜 ∖ 𝑧)〉 ∈ (𝐼 ×
2𝑜)) |
12 | 11 | adantl 481 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) →
〈𝑦,
(1𝑜 ∖ 𝑧)〉 ∈ (𝐼 ×
2𝑜)) |
13 | 8, 12 | s2cld 13466 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) →
〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉 ∈ Word
(𝐼 ×
2𝑜)) |
14 | | splcl 13354 |
. . . . . . 7
⊢ ((𝑥 ∈ Word (𝐼 × 2𝑜) ∧
〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉 ∈ Word
(𝐼 ×
2𝑜)) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
∈ Word (𝐼 ×
2𝑜)) |
15 | 6, 13, 14 | syl2anc 691 |
. . . . . 6
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
∈ Word (𝐼 ×
2𝑜)) |
16 | 3 | efgrcl 17951 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
17 | 16 | simprd 478 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑊 → 𝑊 = Word (𝐼 ×
2𝑜)) |
18 | 17 | ad2antrr 758 |
. . . . . 6
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) → 𝑊 = Word (𝐼 ×
2𝑜)) |
19 | 15, 18 | eleqtrrd 2691 |
. . . . 5
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
∈ 𝑊) |
20 | | brxp 5071 |
. . . . 5
⊢ (𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
↔ (𝑥 ∈ 𝑊 ∧ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
∈ 𝑊)) |
21 | 2, 19, 20 | sylanbrc 695 |
. . . 4
⊢ (((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2𝑜)) → 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)) |
22 | 21 | ralrimivva 2954 |
. . 3
⊢ ((𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥))) → ∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)) |
23 | 22 | rgen2 2958 |
. 2
⊢
∀𝑥 ∈
𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉) |
24 | | fvex 6113 |
. . . . 5
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ∈ V |
25 | 3, 24 | eqeltri 2684 |
. . . 4
⊢ 𝑊 ∈ V |
26 | 25, 25 | xpex 6860 |
. . 3
⊢ (𝑊 × 𝑊) ∈ V |
27 | | ereq1 7636 |
. . . 4
⊢ (𝑟 = (𝑊 × 𝑊) → (𝑟 Er 𝑊 ↔ (𝑊 × 𝑊) Er 𝑊)) |
28 | | breq 4585 |
. . . . . 6
⊢ (𝑟 = (𝑊 × 𝑊) → (𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
↔ 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))) |
29 | 28 | 2ralbidv 2972 |
. . . . 5
⊢ (𝑟 = (𝑊 × 𝑊) → (∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
↔ ∀𝑦 ∈
𝐼 ∀𝑧 ∈ 2𝑜
𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))) |
30 | 29 | 2ralbidv 2972 |
. . . 4
⊢ (𝑟 = (𝑊 × 𝑊) → (∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)
↔ ∀𝑥 ∈
𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))) |
31 | 27, 30 | anbi12d 743 |
. . 3
⊢ (𝑟 = (𝑊 × 𝑊) → ((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))
↔ ((𝑊 × 𝑊) Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)))) |
32 | 26, 31 | spcev 3273 |
. 2
⊢ (((𝑊 × 𝑊) Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥(𝑊 × 𝑊)(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))
→ ∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))) |
33 | 1, 23, 32 | mp2an 704 |
1
⊢
∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)) |