Metamath Proof Explorer


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