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	$$⊢\neg W⟨“\mathrm{I}5”⟩\mathrm{dom}\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		dmv	$$⊢\mathrm{dom}\mathrm{V}=\mathrm{V}$$
2		elirr	$$⊢\neg \mathrm{V}\in \mathrm{V}$$
3	1 2	eqneltri	$$⊢\neg \mathrm{dom}\mathrm{V}\in \mathrm{V}$$
4		opprc2	$$⊢\neg \mathrm{dom}\mathrm{V}\in \mathrm{V}\to ⟨W,\mathrm{dom}\mathrm{V}⟩=\varnothing$$
5	3 4	ax-mp	$$⊢⟨W,\mathrm{dom}\mathrm{V}⟩=\varnothing$$
6		s2cli	$$⊢⟨“\mathrm{I}5”⟩\in \mathrm{Word}\mathrm{V}$$
7		wrdfn	$$⊢⟨“\mathrm{I}5”⟩\in \mathrm{Word}\mathrm{V}\to ⟨“\mathrm{I}5”⟩Fn\left(0..^\left|⟨“\mathrm{I}5”⟩\right|\right)$$
8		fnfun	$$⊢⟨“\mathrm{I}5”⟩Fn\left(0..^\left|⟨“\mathrm{I}5”⟩\right|\right)\to \mathrm{Fun}⟨“\mathrm{I}5”⟩$$
9	6 7 8	mp2b	$$⊢\mathrm{Fun}⟨“\mathrm{I}5”⟩$$
10		0nelfun	$$⊢\mathrm{Fun}⟨“\mathrm{I}5”⟩\to \varnothing \notin ⟨“\mathrm{I}5”⟩$$
11	9 10	ax-mp	$$⊢\varnothing \notin ⟨“\mathrm{I}5”⟩$$
12	11	neli	$$⊢\neg \varnothing \in ⟨“\mathrm{I}5”⟩$$
13	5 12	eqneltri	$$⊢\neg ⟨W,\mathrm{dom}\mathrm{V}⟩\in ⟨“\mathrm{I}5”⟩$$
14		df-br	$$⊢W⟨“\mathrm{I}5”⟩\mathrm{dom}\mathrm{V}\leftrightarrow ⟨W,\mathrm{dom}\mathrm{V}⟩\in ⟨“\mathrm{I}5”⟩$$
15	14	biimpi	$$⊢W⟨“\mathrm{I}5”⟩\mathrm{dom}\mathrm{V}\to ⟨W,\mathrm{dom}\mathrm{V}⟩\in ⟨“\mathrm{I}5”⟩$$
16	13 15	mto	$$⊢\neg W⟨“\mathrm{I}5”⟩\mathrm{dom}\mathrm{V}$$