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 ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) }