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

Metamath Proof Explorer

Theorem frgpnabllem1

Description: Lemma for frgpnabl . (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by AV, 25-Apr-2024)

Ref Expression
Hypotheses frgpnabl.g ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
frgpnabl.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
frgpnabl.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
frgpnabl.p ⊢ + = ( +g ‘ 𝐺 )
frgpnabl.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
frgpnabl.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
frgpnabl.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
frgpnabl.u ⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
frgpnabl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
frgpnabl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
frgpnabl.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐼 )
Assertion frgpnabllem1 ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ( 𝐷 ∩ ( ( 𝑈 ‘ 𝐴 ) + ( 𝑈 ‘ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 frgpnabl.g ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
2 frgpnabl.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
3 frgpnabl.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
4 frgpnabl.p ⊢ + = ( +g ‘ 𝐺 )
5 frgpnabl.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
6 frgpnabl.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
7 frgpnabl.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
8 frgpnabl.u ⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
9 frgpnabl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
10 frgpnabl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
11 frgpnabl.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐼 )
12 0ex ⊢ ∅ ∈ V
13 12 prid1 ⊢ ∅ ∈ { ∅ , 1o }
14 df2o3 ⊢ 2o = { ∅ , 1o }
15 13 14 eleqtrri ⊢ ∅ ∈ 2o
16 opelxpi ⊢ ( ( 𝐴 ∈ 𝐼 ∧ ∅ ∈ 2o ) → ⟨ 𝐴 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
17 10 15 16 sylancl ⊢ ( 𝜑 → ⟨ 𝐴 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
18 opelxpi ⊢ ( ( 𝐵 ∈ 𝐼 ∧ ∅ ∈ 2o ) → ⟨ 𝐵 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
19 11 15 18 sylancl ⊢ ( 𝜑 → ⟨ 𝐵 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
20 17 19 s2cld ⊢ ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) )
21 2on ⊢ 2o ∈ On
22 xpexg ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
23 9 21 22 sylancl ⊢ ( 𝜑 → ( 𝐼 × 2o ) ∈ V )
24 wrdexg ⊢ ( ( 𝐼 × 2o ) ∈ V → Word ( 𝐼 × 2o ) ∈ V )
25 fvi ⊢ ( Word ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
26 23 24 25 3syl ⊢ ( 𝜑 → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
27 2 26 eqtrid ⊢ ( 𝜑 → 𝑊 = Word ( 𝐼 × 2o ) )
28 20 27 eleqtrrd ⊢ ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ 𝑊 )
29 1n0 ⊢ 1o ≠ ∅
30 2cn ⊢ 2 ∈ ℂ
31 30 addlidi ⊢ ( 0 + 2 ) = 2
32 s2len ⊢ ( ♯ ‘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ) = 2
33 31 32 eqtr4i ⊢ ( 0 + 2 ) = ( ♯ ‘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ )
34 2 3 5 6 efgtlen ⊢ ( ( 𝑥 ∈ 𝑊 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) ) → ( ♯ ‘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ) = ( ( ♯ ‘ 𝑥 ) + 2 ) )
35 34 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) ) → ( ♯ ‘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ) = ( ( ♯ ‘ 𝑥 ) + 2 ) )
36 33 35 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) ) → ( 0 + 2 ) = ( ( ♯ ‘ 𝑥 ) + 2 ) )
37 36 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) → ( 0 + 2 ) = ( ( ♯ ‘ 𝑥 ) + 2 ) ) )
38 0cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → 0 ∈ ℂ )
39 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → 𝑥 ∈ 𝑊 )
40 2 efgrcl ⊢ ( 𝑥 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
41 40 simprd ⊢ ( 𝑥 ∈ 𝑊 → 𝑊 = Word ( 𝐼 × 2o ) )
42 41 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → 𝑊 = Word ( 𝐼 × 2o ) )
43 39 42 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → 𝑥 ∈ Word ( 𝐼 × 2o ) )
44 lencl ⊢ ( 𝑥 ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
45 43 44 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
46 45 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( ♯ ‘ 𝑥 ) ∈ ℂ )
47 2cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → 2 ∈ ℂ )
48 38 46 47 addcan2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( ( 0 + 2 ) = ( ( ♯ ‘ 𝑥 ) + 2 ) ↔ 0 = ( ♯ ‘ 𝑥 ) ) )
49 37 48 sylibd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) → 0 = ( ♯ ‘ 𝑥 ) ) )
50 2 3 5 6 efgtf ⊢ ( ∅ ∈ 𝑊 → ( ( 𝑇 ‘ ∅ ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ ∅ ) : ( ( 0 ... ( ♯ ‘ ∅ ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
51 50 adantl ⊢ ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) → ( ( 𝑇 ‘ ∅ ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ ∅ ) : ( ( 0 ... ( ♯ ‘ ∅ ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
52 51 simpld ⊢ ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) → ( 𝑇 ‘ ∅ ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
53 52 rneqd ⊢ ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) → ran ( 𝑇 ‘ ∅ ) = ran ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
54 53 eleq2d ⊢ ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ ∅ ) ↔ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ) )
55 eqid ⊢ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
56 ovex ⊢ ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ∈ V
57 55 56 elrnmpo ⊢ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ↔ ∃ 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∃ 𝑏 ∈ ( 𝐼 × 2o ) ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
58 wrd0 ⊢ ∅ ∈ Word ( 𝐼 × 2o )
59 58 a1i ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ∅ ∈ Word ( 𝐼 × 2o ) )
60 simprr ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑏 ∈ ( 𝐼 × 2o ) )
61 5 efgmf ⊢ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o )
62 61 ffvelcdmi ⊢ ( 𝑏 ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ 𝑏 ) ∈ ( 𝐼 × 2o ) )
63 60 62 syl ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑀 ‘ 𝑏 ) ∈ ( 𝐼 × 2o ) )
64 60 63 s2cld ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
65 ccatidid ⊢ ( ∅ ++ ∅ ) = ∅
66 65 oveq1i ⊢ ( ( ∅ ++ ∅ ) ++ ∅ ) = ( ∅ ++ ∅ )
67 66 65 eqtr2i ⊢ ∅ = ( ( ∅ ++ ∅ ) ++ ∅ )
68 67 a1i ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ∅ = ( ( ∅ ++ ∅ ) ++ ∅ ) )
69 simprl ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) )
70 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
71 70 oveq2i ⊢ ( 0 ... ( ♯ ‘ ∅ ) ) = ( 0 ... 0 )
72 69 71 eleqtrdi ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑎 ∈ ( 0 ... 0 ) )
73 elfz1eq ⊢ ( 𝑎 ∈ ( 0 ... 0 ) → 𝑎 = 0 )
74 72 73 syl ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑎 = 0 )
75 74 70 eqtr4di ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑎 = ( ♯ ‘ ∅ ) )
76 70 oveq2i ⊢ ( 𝑎 + ( ♯ ‘ ∅ ) ) = ( 𝑎 + 0 )
77 0cn ⊢ 0 ∈ ℂ
78 74 77 eqeltrdi ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑎 ∈ ℂ )
79 78 addridd ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑎 + 0 ) = 𝑎 )
80 76 79 eqtr2id ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑎 = ( 𝑎 + ( ♯ ‘ ∅ ) ) )
81 59 59 59 64 68 75 80 splval2 ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) = ( ( ∅ ++ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) ++ ∅ ) )
82 ccatlid ⊢ ( ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ∈ Word ( 𝐼 × 2o ) → ( ∅ ++ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ )
83 82 oveq1d ⊢ ( ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ∈ Word ( 𝐼 × 2o ) → ( ( ∅ ++ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) ++ ∅ ) = ( ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ++ ∅ ) )
84 ccatrid ⊢ ( ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ∈ Word ( 𝐼 × 2o ) → ( ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ++ ∅ ) = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ )
85 83 84 eqtrd ⊢ ( ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ∈ Word ( 𝐼 × 2o ) → ( ( ∅ ++ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) ++ ∅ ) = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ )
86 64 85 syl ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( ∅ ++ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) ++ ∅ ) = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ )
87 81 86 eqtrd ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ )
88 87 eqeq2d ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ↔ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) )
89 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) → 𝐴 ∈ 𝐼 )
90 1on ⊢ 1o ∈ On
91 90 a1i ⊢ ( ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) → 1o ∈ On )
92 simpr ⊢ ( ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ )
93 92 fveq1d ⊢ ( ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ‘ 1 ) = ( ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ‘ 1 ) )
94 opex ⊢ ⟨ 𝐵 , ∅ ⟩ ∈ V
95 s2fv1 ⊢ ( ⟨ 𝐵 , ∅ ⟩ ∈ V → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ‘ 1 ) = ⟨ 𝐵 , ∅ ⟩ )
96 94 95 ax-mp ⊢ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ‘ 1 ) = ⟨ 𝐵 , ∅ ⟩
97 fvex ⊢ ( 𝑀 ‘ 𝑏 ) ∈ V
98 s2fv1 ⊢ ( ( 𝑀 ‘ 𝑏 ) ∈ V → ( ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ‘ 1 ) = ( 𝑀 ‘ 𝑏 ) )
99 97 98 ax-mp ⊢ ( ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ‘ 1 ) = ( 𝑀 ‘ 𝑏 )
100 93 96 99 3eqtr3g ⊢ ( ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) → ⟨ 𝐵 , ∅ ⟩ = ( 𝑀 ‘ 𝑏 ) )
101 92 fveq1d ⊢ ( ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ‘ 0 ) = ( ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ‘ 0 ) )
102 opex ⊢ ⟨ 𝐴 , ∅ ⟩ ∈ V
103 s2fv0 ⊢ ( ⟨ 𝐴 , ∅ ⟩ ∈ V → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ‘ 0 ) = ⟨ 𝐴 , ∅ ⟩ )
104 102 103 ax-mp ⊢ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ‘ 0 ) = ⟨ 𝐴 , ∅ ⟩
105 s2fv0 ⊢ ( 𝑏 ∈ V → ( ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ‘ 0 ) = 𝑏 )
106 105 elv ⊢ ( ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ‘ 0 ) = 𝑏
107 101 104 106 3eqtr3g ⊢ ( ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) → ⟨ 𝐴 , ∅ ⟩ = 𝑏 )
108 107 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) → ( 𝑀 ‘ ⟨ 𝐴 , ∅ ⟩ ) = ( 𝑀 ‘ 𝑏 ) )
109 5 efgmval ⊢ ( ( 𝐴 ∈ 𝐼 ∧ ∅ ∈ 2o ) → ( 𝐴 𝑀 ∅ ) = ⟨ 𝐴 , ( 1o ∖ ∅ ) ⟩ )
110 89 15 109 sylancl ⊢ ( ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) → ( 𝐴 𝑀 ∅ ) = ⟨ 𝐴 , ( 1o ∖ ∅ ) ⟩ )
111 df-ov ⊢ ( 𝐴 𝑀 ∅ ) = ( 𝑀 ‘ ⟨ 𝐴 , ∅ ⟩ )
112 dif0 ⊢ ( 1o ∖ ∅ ) = 1o
113 112 opeq2i ⊢ ⟨ 𝐴 , ( 1o ∖ ∅ ) ⟩ = ⟨ 𝐴 , 1o ⟩
114 110 111 113 3eqtr3g ⊢ ( ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) → ( 𝑀 ‘ ⟨ 𝐴 , ∅ ⟩ ) = ⟨ 𝐴 , 1o ⟩ )
115 100 108 114 3eqtr2rd ⊢ ( ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) → ⟨ 𝐴 , 1o ⟩ = ⟨ 𝐵 , ∅ ⟩ )
116 opthg ⊢ ( ( 𝐴 ∈ 𝐼 ∧ 1o ∈ On ) → ( ⟨ 𝐴 , 1o ⟩ = ⟨ 𝐵 , ∅ ⟩ ↔ ( 𝐴 = 𝐵 ∧ 1o = ∅ ) ) )
117 116 simplbda ⊢ ( ( ( 𝐴 ∈ 𝐼 ∧ 1o ∈ On ) ∧ ⟨ 𝐴 , 1o ⟩ = ⟨ 𝐵 , ∅ ⟩ ) → 1o = ∅ )
118 89 91 115 117 syl21anc ⊢ ( ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) → 1o = ∅ )
119 118 ex ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ → 1o = ∅ ) )
120 88 119 sylbid ⊢ ( ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) → 1o = ∅ ) )
121 120 rexlimdvva ⊢ ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) → ( ∃ 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) ∃ 𝑏 ∈ ( 𝐼 × 2o ) ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) → 1o = ∅ ) )
122 57 121 biimtrid ⊢ ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ∅ ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ∅ splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) → 1o = ∅ ) )
123 54 122 sylbid ⊢ ( ( 𝜑 ∧ ∅ ∈ 𝑊 ) → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ ∅ ) → 1o = ∅ ) )
124 123 expimpd ⊢ ( 𝜑 → ( ( ∅ ∈ 𝑊 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ ∅ ) ) → 1o = ∅ ) )
125 hasheq0 ⊢ ( 𝑥 ∈ V → ( ( ♯ ‘ 𝑥 ) = 0 ↔ 𝑥 = ∅ ) )
126 125 elv ⊢ ( ( ♯ ‘ 𝑥 ) = 0 ↔ 𝑥 = ∅ )
127 eleq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ 𝑊 ↔ ∅ ∈ 𝑊 ) )
128 fveq2 ⊢ ( 𝑥 = ∅ → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ ∅ ) )
129 128 rneqd ⊢ ( 𝑥 = ∅ → ran ( 𝑇 ‘ 𝑥 ) = ran ( 𝑇 ‘ ∅ ) )
130 129 eleq2d ⊢ ( 𝑥 = ∅ → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) ↔ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ ∅ ) ) )
131 127 130 anbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ∈ 𝑊 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) ) ↔ ( ∅ ∈ 𝑊 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ ∅ ) ) ) )
132 126 131 sylbi ⊢ ( ( ♯ ‘ 𝑥 ) = 0 → ( ( 𝑥 ∈ 𝑊 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) ) ↔ ( ∅ ∈ 𝑊 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ ∅ ) ) ) )
133 132 eqcoms ⊢ ( 0 = ( ♯ ‘ 𝑥 ) → ( ( 𝑥 ∈ 𝑊 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) ) ↔ ( ∅ ∈ 𝑊 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ ∅ ) ) ) )
134 133 imbi1d ⊢ ( 0 = ( ♯ ‘ 𝑥 ) → ( ( ( 𝑥 ∈ 𝑊 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) ) → 1o = ∅ ) ↔ ( ( ∅ ∈ 𝑊 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ ∅ ) ) → 1o = ∅ ) ) )
135 124 134 syl5ibrcom ⊢ ( 𝜑 → ( 0 = ( ♯ ‘ 𝑥 ) → ( ( 𝑥 ∈ 𝑊 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) ) → 1o = ∅ ) ) )
136 135 com23 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑊 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) ) → ( 0 = ( ♯ ‘ 𝑥 ) → 1o = ∅ ) ) )
137 136 expdimp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) → ( 0 = ( ♯ ‘ 𝑥 ) → 1o = ∅ ) ) )
138 49 137 mpdd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) → 1o = ∅ ) )
139 138 necon3ad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ( 1o ≠ ∅ → ¬ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) ) )
140 29 139 mpi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑊 ) → ¬ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) )
141 140 nrexdv ⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ 𝑊 ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) )
142 eliun ⊢ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝑊 ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ran ( 𝑇 ‘ 𝑥 ) )
143 141 142 sylnibr ⊢ ( 𝜑 → ¬ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
144 28 143 eldifd ⊢ ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) )
145 144 7 eleqtrrdi ⊢ ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ 𝐷 )
146 df-s2 ⊢ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ++ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ )
147 2 3 efger ⊢ ∼ Er 𝑊
148 147 a1i ⊢ ( 𝜑 → ∼ Er 𝑊 )
149 148 28 erref ⊢ ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∼ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ )
150 146 149 eqbrtrrid ⊢ ( 𝜑 → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ++ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ) ∼ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ )
151 146 ovexi ⊢ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ V
152 ovex ⊢ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ++ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ) ∈ V
153 151 152 elec ⊢ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ [ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ++ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ) ] ∼ ↔ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ++ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ) ∼ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ )
154 150 153 sylibr ⊢ ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ [ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ++ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ) ] ∼ )
155 3 8 vrgpval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐴 ) = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ )
156 9 10 155 syl2anc ⊢ ( 𝜑 → ( 𝑈 ‘ 𝐴 ) = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ )
157 3 8 vrgpval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐵 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐵 ) = [ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ] ∼ )
158 9 11 157 syl2anc ⊢ ( 𝜑 → ( 𝑈 ‘ 𝐵 ) = [ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ] ∼ )
159 156 158 oveq12d ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝐴 ) + ( 𝑈 ‘ 𝐵 ) ) = ( [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ + [ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ] ∼ ) )
160 17 s1cld ⊢ ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) )
161 160 27 eleqtrrd ⊢ ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ 𝑊 )
162 19 s1cld ⊢ ( 𝜑 → ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) )
163 162 27 eleqtrrd ⊢ ( 𝜑 → ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ 𝑊 )
164 2 1 3 4 frgpadd ⊢ ( ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ 𝑊 ∧ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ 𝑊 ) → ( [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ + [ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ] ∼ ) = [ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ++ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ) ] ∼ )
165 161 163 164 syl2anc ⊢ ( 𝜑 → ( [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ + [ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ] ∼ ) = [ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ++ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ) ] ∼ )
166 159 165 eqtrd ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝐴 ) + ( 𝑈 ‘ 𝐵 ) ) = [ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ++ ⟨“ ⟨ 𝐵 , ∅ ⟩ ”⟩ ) ] ∼ )
167 154 166 eleqtrrd ⊢ ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ( ( 𝑈 ‘ 𝐴 ) + ( 𝑈 ‘ 𝐵 ) ) )
168 145 167 elind ⊢ ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ( 𝐷 ∩ ( ( 𝑈 ‘ 𝐴 ) + ( 𝑈 ‘ 𝐵 ) ) ) )