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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | s4cli | ⊢ 〈“ 〈“ 〈“ 𝑁 𝑒 𝑣 𝑒 𝑟 ”〉 〈“ 𝑔 𝑜 𝑛 𝑛 𝑎 ”〉 〈“ 𝑔 𝑖 𝑣 𝑒 ”〉 〈“ 𝑦 𝑜 𝑢 ”〉 〈“ 𝑢 𝑝 ”〉 ”〉 〈“ 〈“ 𝑁 𝑒 𝑣 𝑒 𝑟 ”〉 〈“ 𝑔 𝑜 𝑛 𝑛 𝑎 ”〉 〈“ 𝑙 𝑒 𝑡 ”〉 〈“ 𝑦 𝑜 𝑢 ”〉 〈“ 𝑑 𝑜 𝑤 𝑛 ”〉 ”〉 〈“ 〈“ 𝑁 𝑒 𝑣 𝑒 𝑟 ”〉 〈“ 𝑔 𝑜 𝑛 𝑛 𝑎 ”〉 〈“ 𝑡 𝑢 𝑟 𝑛 ”〉 〈“ 𝑎 𝑟 𝑜 𝑢 𝑛 𝑑 ”〉 〈“ 𝑎 𝑛 𝑑 ”〉 ”〉 〈“ 〈“ 𝑑 𝑒 𝑠 𝑒 𝑟 𝑡 ”〉 〈“ 𝑦 𝑜 𝑢 ! ”〉 ”〉 ”〉 ∈ Word V | |
2 | prex | ⊢ { 〈“ 𝐴 𝑝 𝑟 𝑖 𝑙 ”〉 , 〈“ 𝑓 𝑜 𝑜 𝑙 𝑠 ! ”〉 } ∈ V | |
3 | 1 2 | iddii | ⊢ { 〈“ 𝐴 𝑝 𝑟 𝑖 𝑙 ”〉 , 〈“ 𝑓 𝑜 𝑜 𝑙 𝑠 ! ”〉 } ∈ V |