let p be MP-variable; for A, B being MP-wff holds
( @ p <> 'not' A & @ p <> (#) A & @ p <> A '&' B )
let A, B be MP-wff; ( @ p <> 'not' A & @ p <> (#) A & @ p <> A '&' B )
set e2 = elementary_tree 2;
set e1 = elementary_tree 1;
set e0 = elementary_tree 0 ;
A1:
dom (@ p) = elementary_tree 0
by FUNCOP_1:19;
A2:
<*0 *> in elementary_tree 1
by TARSKI:def 2, TREES_1:88;
dom ((elementary_tree 1) --> [1,0 ]) = elementary_tree 1
by FUNCOP_1:19;
then
dom ('not' A) = (elementary_tree 1) with-replacement <*0 *>,(dom A)
by A2, TREES_2:def 12;
then
<*0 *> in dom ('not' A)
by A2, TREES_1:def 12;
hence
@ p <> 'not' A
by A1, TARSKI:def 1, TREES_1:56; ( @ p <> (#) A & @ p <> A '&' B )
dom ((elementary_tree 1) --> [1,1]) = elementary_tree 1
by FUNCOP_1:19;
then
dom ((#) A) = (elementary_tree 1) with-replacement <*0 *>,(dom A)
by A2, TREES_2:def 12;
then
<*0 *> in dom ((#) A)
by A2, TREES_1:def 12;
hence
@ p <> (#) A
by A1, TARSKI:def 1, TREES_1:56; @ p <> A '&' B
set y = ((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A;
A3:
( <*1*> in elementary_tree 2 & not <*0 *> is_a_proper_prefix_of <*1*> )
by TREES_1:55, TREES_1:89;
A4:
( <*0 *> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0 ]) = elementary_tree 2 )
by FUNCOP_1:19, TREES_1:55;
then
dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) = (dom ((elementary_tree 2) --> [2,0 ])) with-replacement <*0 *>,(dom A)
by TREES_2:def 12;
then A5:
<*1*> in dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A)
by A4, A3, TREES_1:def 12;
then
dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A)) with-replacement <*1*>,(dom B)
by TREES_2:def 12;
then
<*1*> in dom (A '&' B)
by A5, TREES_1:def 12;
hence
@ p <> A '&' B
by A1, TARSKI:def 1, TREES_1:56; verum