Metamath Proof Explorer

Theorem efglem

Description: Lemma for efgval . (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypothesis efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
Assertion efglem ∃ 𝑟 ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) )

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2 xpider ⊢ ( 𝑊 × 𝑊 ) Er 𝑊
3 simpll ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) ) → 𝑥 ∈ 𝑊 )
4 fviss ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
5 1 4 eqsstri ⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
6 5 3 sseldi ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) ) → 𝑥 ∈ Word ( 𝐼 × 2o ) )
7 opelxpi ⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐼 × 2o ) )
8 7 adantl ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐼 × 2o ) )
9 2oconcl ⊢ ( 𝑧 ∈ 2o → ( 1o ∖ 𝑧 ) ∈ 2o )
10 opelxpi ⊢ ( ( 𝑦 ∈ 𝐼 ∧ ( 1o ∖ 𝑧 ) ∈ 2o ) → ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ∈ ( 𝐼 × 2o ) )
11 9 10 sylan2 ⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) → ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ∈ ( 𝐼 × 2o ) )
12 11 adantl ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) ) → ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ∈ ( 𝐼 × 2o ) )
13 8 12 s2cld ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) ) → ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) )
14 splcl ⊢ ( ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ∈ Word ( 𝐼 × 2o ) )
15 6 13 14 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) ) → ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ∈ Word ( 𝐼 × 2o ) )
16 1 efgrcl ⊢ ( 𝑥 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
17 16 simprd ⊢ ( 𝑥 ∈ 𝑊 → 𝑊 = Word ( 𝐼 × 2o ) )
18 17 ad2antrr ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) ) → 𝑊 = Word ( 𝐼 × 2o ) )
19 15 18 eleqtrrd ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) ) → ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ∈ 𝑊 )
20 brxp ⊢ ( 𝑥 ( 𝑊 × 𝑊 ) ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ↔ ( 𝑥 ∈ 𝑊 ∧ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ∈ 𝑊 ) )
21 3 19 20 sylanbrc ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) ) → 𝑥 ( 𝑊 × 𝑊 ) ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) )
22 21 ralrimivva ⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 ( 𝑊 × 𝑊 ) ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) )
23 22 rgen2 ⊢ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 ( 𝑊 × 𝑊 ) ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ )
24 1 fvexi ⊢ 𝑊 ∈ V
25 24 24 xpex ⊢ ( 𝑊 × 𝑊 ) ∈ V
26 ereq1 ⊢ ( 𝑟 = ( 𝑊 × 𝑊 ) → ( 𝑟 Er 𝑊 ↔ ( 𝑊 × 𝑊 ) Er 𝑊 ) )
27 breq ⊢ ( 𝑟 = ( 𝑊 × 𝑊 ) → ( 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ↔ 𝑥 ( 𝑊 × 𝑊 ) ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) )
28 27 2ralbidv ⊢ ( 𝑟 = ( 𝑊 × 𝑊 ) → ( ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ↔ ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 ( 𝑊 × 𝑊 ) ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) )
29 28 2ralbidv ⊢ ( 𝑟 = ( 𝑊 × 𝑊 ) → ( ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ↔ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 ( 𝑊 × 𝑊 ) ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) )
30 26 29 anbi12d ⊢ ( 𝑟 = ( 𝑊 × 𝑊 ) → ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) ↔ ( ( 𝑊 × 𝑊 ) Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 ( 𝑊 × 𝑊 ) ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) ) )
31 25 30 spcev ⊢ ( ( ( 𝑊 × 𝑊 ) Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 ( 𝑊 × 𝑊 ) ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) → ∃ 𝑟 ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) )
32 2 23 31 mp2an ⊢ ∃ 𝑟 ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) )