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	|- -. W <" _I 5 "> dom _V

Proof

Step	Hyp	Ref	Expression
1		dmv	|- dom _V = _V
2		elirr	|- -. _V e. _V
3	1 2	eqneltri	|- -. dom _V e. _V
4		opprc2	|- ( -. dom _V e. _V -> <. W , dom _V >. = (/) )
5	3 4	ax-mp	|- <. W , dom _V >. = (/)
6		s2cli	|- <" _I 5 "> e. Word _V
7		wrdfn	|- ( <" _I 5 "> e. 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 "> -> (/) e/ <" _I 5 "> )
11	9 10	ax-mp	|- (/) e/ <" _I 5 ">
12	11	neli	|- -. (/) e. <" _I 5 ">
13	5 12	eqneltri	|- -. <. W , dom _V >. e. <" _I 5 ">
14		df-br	|- ( W <" _I 5 "> dom _V <-> <. W , dom _V >. e. <" _I 5 "> )
15	14	biimpi	|- ( W <" _I 5 "> dom _V -> <. W , dom _V >. e. <" _I 5 "> )
16	13 15	mto	|- -. W <" _I 5 "> dom _V