Rayo name of 65536 with 346 symbols

Edit: I shouldn't put the number of symbols in the title, because if i find a mistake, i can't fix the title. So it's actually 387 symbols.

Edit 2: Emk found another mistake, but fixing it reduces the number of symbols to 346.

Edit 3: C7X changed the title to the correct one. Thank you C7X!

P-bot recently found a Rayo name for 65536 with only 442 symbols: https://googology.wikia.org/wiki/User_blog:P%E9%80%B2%E5%A4%A7%E5%A5%BD%E3%81%8Dbot/Rayo_name_of_65536

It can be reduced to 426 symbols by changing the IsOrdinal(x) to a shorter version, which was discovered independently by Emk and me. But P-bot used surjections, and a shorter result can be achieved with bijections. So instead of ●UniquelyWedges●To●(x_i,x_j,x_k), i created ●Wedges●With●(x_i,x_j,x_k), which has one addition: (¬∃x_l((x_l≠x_j∧●Wedges●To●(x_i,x_l,x_k))))

After Emk found a mistake, i had to remove the restriction that x_j and x_k must be different in ●Wedges●To●(x_i,x_j,x_k), and i shortened ●Wedges●With●(x_i,x_j,x_k) by joining the two parts that were almost identical, but with x_j and x_k swapped.

IsIncludedInV₅(x_i) is a modification of P-bot's ●IsIncludedInFourthPowerOf0(x_i), which we get by adding "∃x_o((x_o∈x_j∧" before the FormChain and adding "))" at the end. It's basically just making the chain 1 variable longer, which adds 10 symbols.

Is65536(x_i) now says that x_i is an ordinal and that there is an x_k such that for everything in x_i, x_k wedges it with something in V₅, and for everything in V₅, x_k wedges it with something in x_i. In other words, x_k is a bijection from x_i to V₅.

IsOrdinal(xi)	(¬∃xj(∃xk(((xk∈xj∧xj∈xi)∧(¬(xk∈xi∧(¬∃xl((xl∈xk∧(¬xl∈xj))))))))))	3+4+4+3+3+3+3+3+3 +3+3+4+3+3+3+3 = 51
IsV5(xi)	IsIncludedInV5(xi)∧●IncludesFifthPowerOf0(xi)	60+3+66 = 129
●Wedges●To●(xi,xj,xk)	∃xm((xj∈xm∧xk∈xm)∧xm∈xi)	4+3+3+3+3+3=19
●Wedges●With●(xi,xj,xk)	●Wedges●To●(xi,xj,xk)∧(¬∃xl(((xl≠xj∧xl≠xk)∧ ∃xm(((¬((¬xj∈xm)∧(¬xk∈xm)))∧xl∈xm)∧xm∈xi))))	19+3+3+4+6+3+6+3+4 +3+3+3+3+3+3+3+3+3 +3 = 81
Is65536(xi)	IsOrdinal(xi)∧∃xj((IsV5(xj)∧∃xk((¬∃xl(((¬((¬xl∈xi)∧(¬xl∈xj)))∧ (¬∃xm((((¬(xl∈xi∧(¬xm∈xj)))∧(¬(xl∈xj∧(¬xm∈xi))))∧ ●Wedges●With●(xk,xl,xm))))))))))	51+3+4+129+3+4+3+4 +3+3+3+3+3+3+3+3+4 +3+3+3+3+3+3+3+3+3 +3+3+3+81 = 346

Of course, we can change V₅ to V_n+1 to get a formula for 2↑↑n, which has 266+20n symbols.