Theorem aprilfools2025

Description: An abuse of notation. (Contributed by Prof. Loof Lirpa, 1-Apr-2025) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	aprilfools2025	⊢ { ⟨“ 𝐴 𝑝 𝑟 𝑖 𝑙 ”⟩ , ⟨“ 𝑓 𝑜 𝑜 𝑙 𝑠 ! ”⟩ } ∈ V

Proof

Step	Hyp	Ref	Expression
1		s4cli	⊢ ⟨“ ⟨“ ⟨“ 𝑁 𝑒 𝑣 𝑒 𝑟 ”⟩ ⟨“ 𝑔 𝑜 𝑛 𝑛 𝑎 ”⟩ ⟨“ 𝑔 𝑖 𝑣 𝑒 ”⟩ ⟨“ 𝑦 𝑜 𝑢 ”⟩ ⟨“ 𝑢 𝑝 ”⟩ ”⟩ ⟨“ ⟨“ 𝑁 𝑒 𝑣 𝑒 𝑟 ”⟩ ⟨“ 𝑔 𝑜 𝑛 𝑛 𝑎 ”⟩ ⟨“ 𝑙 𝑒 𝑡 ”⟩ ⟨“ 𝑦 𝑜 𝑢 ”⟩ ⟨“ 𝑑 𝑜 𝑤 𝑛 ”⟩ ”⟩ ⟨“ ⟨“ 𝑁 𝑒 𝑣 𝑒 𝑟 ”⟩ ⟨“ 𝑔 𝑜 𝑛 𝑛 𝑎 ”⟩ ⟨“ 𝑡 𝑢 𝑟 𝑛 ”⟩ ⟨“ 𝑎 𝑟 𝑜 𝑢 𝑛 𝑑 ”⟩ ⟨“ 𝑎 𝑛 𝑑 ”⟩ ”⟩ ⟨“ ⟨“ 𝑑 𝑒 𝑠 𝑒 𝑟 𝑡 ”⟩ ⟨“ 𝑦 𝑜 𝑢 ! ”⟩ ”⟩ ”⟩ ∈ Word V
2		prex	⊢ { ⟨“ 𝐴 𝑝 𝑟 𝑖 𝑙 ”⟩ , ⟨“ 𝑓 𝑜 𝑜 𝑙 𝑠 ! ”⟩ } ∈ V
3	1 2	iddii	⊢ { ⟨“ 𝐴 𝑝 𝑟 𝑖 𝑙 ”⟩ , ⟨“ 𝑓 𝑜 𝑜 𝑙 𝑠 ! ”⟩ } ∈ V