This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efgval

Description: Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
Assertion efgval ∼ = ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) }

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2 efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
3 vex ⊢ 𝑖 ∈ V
4 2on ⊢ 2o ∈ On
5 4 elexi ⊢ 2o ∈ V
6 3 5 xpex ⊢ ( 𝑖 × 2o ) ∈ V
7 wrdexg ⊢ ( ( 𝑖 × 2o ) ∈ V → Word ( 𝑖 × 2o ) ∈ V )
8 fvi ⊢ ( Word ( 𝑖 × 2o ) ∈ V → ( I ‘ Word ( 𝑖 × 2o ) ) = Word ( 𝑖 × 2o ) )
9 6 7 8 mp2b ⊢ ( I ‘ Word ( 𝑖 × 2o ) ) = Word ( 𝑖 × 2o )
10 xpeq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 × 2o ) = ( 𝐼 × 2o ) )
11 wrdeq ⊢ ( ( 𝑖 × 2o ) = ( 𝐼 × 2o ) → Word ( 𝑖 × 2o ) = Word ( 𝐼 × 2o ) )
12 10 11 syl ⊢ ( 𝑖 = 𝐼 → Word ( 𝑖 × 2o ) = Word ( 𝐼 × 2o ) )
13 12 fveq2d ⊢ ( 𝑖 = 𝐼 → ( I ‘ Word ( 𝑖 × 2o ) ) = ( I ‘ Word ( 𝐼 × 2o ) ) )
14 9 13 eqtr3id ⊢ ( 𝑖 = 𝐼 → Word ( 𝑖 × 2o ) = ( I ‘ Word ( 𝐼 × 2o ) ) )
15 14 1 eqtr4di ⊢ ( 𝑖 = 𝐼 → Word ( 𝑖 × 2o ) = 𝑊 )
16 ereq2 ⊢ ( Word ( 𝑖 × 2o ) = 𝑊 → ( 𝑟 Er Word ( 𝑖 × 2o ) ↔ 𝑟 Er 𝑊 ) )
17 15 16 syl ⊢ ( 𝑖 = 𝐼 → ( 𝑟 Er Word ( 𝑖 × 2o ) ↔ 𝑟 Er 𝑊 ) )
18 raleq ⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ↔ ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) )
19 18 ralbidv ⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ↔ ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) )
20 15 19 raleqbidv ⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ↔ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) )
21 17 20 anbi12d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) ↔ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) ) )
22 21 abbidv ⊢ ( 𝑖 = 𝐼 → { 𝑟 ∣ ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } = { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } )
23 22 inteqd ⊢ ( 𝑖 = 𝐼 → ∩ { 𝑟 ∣ ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } = ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } )
24 df-efg ⊢ ~FG = ( 𝑖 ∈ V ↦ ∩ { 𝑟 ∣ ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } )
25 1 efglem ⊢ ∃ 𝑟 ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) )
26 intexab ⊢ ( ∃ 𝑟 ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) ↔ ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } ∈ V )
27 25 26 mpbi ⊢ ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } ∈ V
28 23 24 27 fvmpt ⊢ ( 𝐼 ∈ V → ( ~FG ‘ 𝐼 ) = ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } )
29 fvprc ⊢ ( ¬ 𝐼 ∈ V → ( ~FG ‘ 𝐼 ) = ∅ )
30 abn0 ⊢ ( { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } ≠ ∅ ↔ ∃ 𝑟 ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) )
31 25 30 mpbir ⊢ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } ≠ ∅
32 intssuni ⊢ ( { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } ≠ ∅ → ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } ⊆ ∪ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } )
33 31 32 ax-mp ⊢ ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } ⊆ ∪ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) }
34 erssxp ⊢ ( 𝑟 Er 𝑊 → 𝑟 ⊆ ( 𝑊 × 𝑊 ) )
35 1 efgrcl ⊢ ( 𝑥 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
36 35 simpld ⊢ ( 𝑥 ∈ 𝑊 → 𝐼 ∈ V )
37 36 con3i ⊢ ( ¬ 𝐼 ∈ V → ¬ 𝑥 ∈ 𝑊 )
38 37 eq0rdv ⊢ ( ¬ 𝐼 ∈ V → 𝑊 = ∅ )
39 38 xpeq2d ⊢ ( ¬ 𝐼 ∈ V → ( 𝑊 × 𝑊 ) = ( 𝑊 × ∅ ) )
40 xp0 ⊢ ( 𝑊 × ∅ ) = ∅
41 39 40 eqtrdi ⊢ ( ¬ 𝐼 ∈ V → ( 𝑊 × 𝑊 ) = ∅ )
42 ss0b ⊢ ( ( 𝑊 × 𝑊 ) ⊆ ∅ ↔ ( 𝑊 × 𝑊 ) = ∅ )
43 41 42 sylibr ⊢ ( ¬ 𝐼 ∈ V → ( 𝑊 × 𝑊 ) ⊆ ∅ )
44 34 43 sylan9ssr ⊢ ( ( ¬ 𝐼 ∈ V ∧ 𝑟 Er 𝑊 ) → 𝑟 ⊆ ∅ )
45 44 ex ⊢ ( ¬ 𝐼 ∈ V → ( 𝑟 Er 𝑊 → 𝑟 ⊆ ∅ ) )
46 45 adantrd ⊢ ( ¬ 𝐼 ∈ V → ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) → 𝑟 ⊆ ∅ ) )
47 46 alrimiv ⊢ ( ¬ 𝐼 ∈ V → ∀ 𝑟 ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) → 𝑟 ⊆ ∅ ) )
48 sseq1 ⊢ ( 𝑤 = 𝑟 → ( 𝑤 ⊆ ∅ ↔ 𝑟 ⊆ ∅ ) )
49 48 ralab2 ⊢ ( ∀ 𝑤 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } 𝑤 ⊆ ∅ ↔ ∀ 𝑟 ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) → 𝑟 ⊆ ∅ ) )
50 47 49 sylibr ⊢ ( ¬ 𝐼 ∈ V → ∀ 𝑤 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } 𝑤 ⊆ ∅ )
51 unissb ⊢ ( ∪ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } ⊆ ∅ ↔ ∀ 𝑤 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } 𝑤 ⊆ ∅ )
52 50 51 sylibr ⊢ ( ¬ 𝐼 ∈ V → ∪ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } ⊆ ∅ )
53 33 52 sstrid ⊢ ( ¬ 𝐼 ∈ V → ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } ⊆ ∅ )
54 ss0 ⊢ ( ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } ⊆ ∅ → ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } = ∅ )
55 53 54 syl ⊢ ( ¬ 𝐼 ∈ V → ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } = ∅ )
56 29 55 eqtr4d ⊢ ( ¬ 𝐼 ∈ V → ( ~FG ‘ 𝐼 ) = ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } )
57 28 56 pm2.61i ⊢ ( ~FG ‘ 𝐼 ) = ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) }
58 2 57 eqtri ⊢ ∼ = ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) }