let A be MP-wff; :: thesis: ( not card (dom A) = 1 or A = VERUM or ex p being MP-variable st A = @ p )
assume card (dom A) = 1 ; :: thesis: ( A = VERUM or ex p being MP-variable st A = @ p )
then consider x being object such that
A1: dom A = {x} by CARD_2:42;
reconsider x = x as Element of dom A by A1, TARSKI:def 1;
A2: {} in dom A by TREES_1:22;
then A3: dom A = elementary_tree 0 by A1, TARSKI:def 1, TREES_1:29;
A4: dom A = {{}} by A2, A1, TARSKI:def 1;
succ x = {}
proof
set y = the Element of succ x;
assume not succ x = {} ; :: thesis: contradiction
then A5: the Element of succ x in succ x ;
succ x = { (x ^ <*n*>) where n is Nat : x ^ <*n*> in dom A } by TREES_2:def 5;
then ex n being Nat st
( the Element of succ x = x ^ <*n*> & x ^ <*n*> in dom A ) by A5;
hence contradiction by A4, TARSKI:def 1; :: thesis: verum
end;
then A6: branchdeg x = 0 by CARD_1:27, TREES_2:def 12;
now :: thesis: ( A = VERUM or ex p being MP-variable st A = @ p )
per cases ( A . x = [0,0] or ex n being Nat st A . x = [3,n] ) by A6, Def5;
suppose A . x = [0,0] ; :: thesis: ( A = VERUM or ex p being MP-variable st A = @ p )
then for z being object st z in dom A holds
A . z = [0,0] by A1, TARSKI:def 1;
hence ( A = VERUM or ex p being MP-variable st A = @ p ) by A3, FUNCOP_1:11; :: thesis: verum
end;
suppose ex n being Nat st A . x = [3,n] ; :: thesis: ( A = VERUM or ex p being MP-variable st A = @ p )
then consider n being Nat such that
A7: A . x = [3,n] ;
( 3 in NAT & n in NAT ) by ORDINAL1:def 12;
then reconsider p = [3,n] as MP-variable by ZFMISC_1:105;
for z being object st z in dom A holds
A . z = [3,n] by A1, A7, TARSKI:def 1;
then A = @ p by A3, FUNCOP_1:11;
hence ( A = VERUM or ex p being MP-variable st A = @ p ) ; :: thesis: verum
end;
end;
end;
hence ( A = VERUM or ex p being MP-variable st A = @ p ) ; :: thesis: verum