Theorem nowisdomv

Description: One's wisdom on matters of the universe can be refuted on April Fool's day. (Contributed by Prof. Loof Lirpa, 1-Apr-2026) (New usage is discouraged.)

	Ref	Expression
Assertion	nowisdomv	⊢ ¬ 𝑊 ⟨“ I 5 ”⟩ dom V

Proof

Step	Hyp	Ref	Expression
1		dmv	⊢ dom V = V
2		elirr	⊢ ¬ V ∈ V
3	1 2	eqneltri	⊢ ¬ dom V ∈ V
4		opprc2	⊢ ( ¬ dom V ∈ V → ⟨ 𝑊 , dom V ⟩ = ∅ )
5	3 4	ax-mp	⊢ ⟨ 𝑊 , dom V ⟩ = ∅
6		s2cli	⊢ ⟨“ I 5 ”⟩ ∈ Word V
7		wrdfn	⊢ ( ⟨“ I 5 ”⟩ ∈ Word V → ⟨“ I 5 ”⟩ Fn ( 0 ..^ ( ♯ ‘ ⟨“ I 5 ”⟩ ) ) )
8		fnfun	⊢ ( ⟨“ I 5 ”⟩ Fn ( 0 ..^ ( ♯ ‘ ⟨“ I 5 ”⟩ ) ) → Fun ⟨“ I 5 ”⟩ )
9	6 7 8	mp2b	⊢ Fun ⟨“ I 5 ”⟩
10		0nelfun	⊢ ( Fun ⟨“ I 5 ”⟩ → ∅ ∉ ⟨“ I 5 ”⟩ )
11	9 10	ax-mp	⊢ ∅ ∉ ⟨“ I 5 ”⟩
12	11	neli	⊢ ¬ ∅ ∈ ⟨“ I 5 ”⟩
13	5 12	eqneltri	⊢ ¬ ⟨ 𝑊 , dom V ⟩ ∈ ⟨“ I 5 ”⟩
14		df-br	⊢ ( 𝑊 ⟨“ I 5 ”⟩ dom V ↔ ⟨ 𝑊 , dom V ⟩ ∈ ⟨“ I 5 ”⟩ )
15	14	biimpi	⊢ ( 𝑊 ⟨“ I 5 ”⟩ dom V → ⟨ 𝑊 , dom V ⟩ ∈ ⟨“ I 5 ”⟩ )
16	13 15	mto	⊢ ¬ 𝑊 ⟨“ I 5 ”⟩ dom V