Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

shorten vtoclg, vtoclegft, vtoclf #4605

Merged
merged 4 commits into from
Jan 27, 2025
Merged

shorten vtoclg, vtoclegft, vtoclf #4605

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a0ce14f
shorten vtoclg
wlammen Jan 26, 2025
c943de7
shorten vtoclegft
wlammen Jan 26, 2025
2a9abd9
typo
wlammen Jan 26, 2025
382f24e
shorten vtoclf
wlammen Jan 26, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 7 additions & 1 deletion discouraged
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19523,7 +19523,10 @@ New usage of "vsfval" is discouraged (4 uses).
New usage of "vtocl3gaOLD" is discouraged (0 uses).
New usage of "vtoclALT" is discouraged (0 uses).
New usage of "vtocldOLD" is discouraged (0 uses).
New usage of "vtoclegftOLD" is discouraged (0 uses).
New usage of "vtoclfOLD" is discouraged (0 uses).
New usage of "vtoclgOLD" is discouraged (0 uses).
New usage of "vtoclgOLDOLD" is discouraged (0 uses).
New usage of "vtxdusgr0edgnelALT" is discouraged (0 uses).
New usage of "w-bnj13" is discouraged (5 uses).
New usage of "w-bnj15" is discouraged (92 uses).
Expand Down Expand Up @@ -21557,7 +21560,10 @@ Proof modification of "vn0ALT" is discouraged (6 steps).
Proof modification of "vtocl3gaOLD" is discouraged (45 steps).
Proof modification of "vtoclALT" is discouraged (11 steps).
Proof modification of "vtocldOLD" is discouraged (21 steps).
Proof modification of "vtoclgOLD" is discouraged (11 steps).
Proof modification of "vtoclegftOLD" is discouraged (50 steps).
Proof modification of "vtoclfOLD" is discouraged (28 steps).
Proof modification of "vtoclgOLD" is discouraged (25 steps).
Proof modification of "vtoclgOLDOLD" is discouraged (11 steps).
Proof modification of "vtxdusgr0edgnelALT" is discouraged (94 steps).
Proof modification of "wfiOLD" is discouraged (227 steps).
Proof modification of "wfis2fgOLD" is discouraged (51 steps).
Expand Down
107 changes: 69 additions & 38 deletions set.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26764,10 +26764,10 @@ generally appear in a single form (either definitional, but more often
~ ax-11 , see ~ sbc5ALT for more details. (Revised by SN,
2-Sep-2024.) $)
clelab $p |- ( A e. { x | ph } <-> E. x ( x = A /\ ph ) ) $=
( vy cab wcel cv wceq wex elisset exsimpl eqeq1 cbvexvw sylib weq df-clab
wa wb wsb sb5 bitri eleq1 eqeq2 anbi1d exbidv bibi12d exlimiv pm5.21nii
mpbii ) CABEZFZDGZCHZDIZBGZCHZAQZBIZDCUJJURUPBIUNUPABKUPUMBDUOULCLMNUMUKU
RRZDUMULUJFZBDOZAQZBIZRUSUTABDSVCADBPABDTUAUMUTUKVCURULCUJUBUMVBUQBUMVAUP
( vy cab wcel cv wceq wex wa elissetv exsimpl eqeq1 cbvexvw sylib weq wsb
wb df-clab sb5 bitri eleq1 eqeq2 anbi1d exbidv bibi12d exlimiv pm5.21nii
mpbii ) CABEZFZDGZCHZDIZBGZCHZAJZBIZDCUJKURUPBIUNUPABLUPUMBDUOULCMNOUMUKU
RRZDUMULUJFZBDPZAJZBIZRUSUTABDQVCADBSABDTUAUMUTUKVCURULCUJUBUMVBUQBUMVAUP
AULCUOUCUDUEUFUIUGUH $.
$( $j usage 'clelab' avoids 'ax-11'; $)

Expand Down Expand Up @@ -32248,9 +32248,9 @@ general is seen either by substitution (when the variable ` V ` has no
$( If two classes each contain another class, then both contain some set.
(Contributed by Alan Sare, 24-Oct-2011.) $)
elex22 $p |- ( ( A e. B /\ A e. C ) -> E. x ( x e. B /\ x e. C ) ) $=
( wcel wa cv wceq wi wal eleq1a anim12ii alrimiv elisset adantr exim sylc
wex ) BCEZBDEZFZAGZBHZUBCEZUBDEZFZIZAJUCARZUFARUAUGASUCUDTUEBCUBKBDUBKLMS
UHTABCNOUCUFAPQ $.
( wcel wa cv wceq wi wal wex eleq1a anim12ii alrimiv elissetv adantr exim
sylc ) BCEZBDEZFZAGZBHZUBCEZUBDEZFZIZAJUCAKZUFAKUAUGASUCUDTUEBCUBLBDUBLMN
SUHTABCOPUCUFAQR $.
$}

$( A proper class doesn't belong to any class. (Contributed by Glauco
Expand Down Expand Up @@ -32862,15 +32862,42 @@ general is seen either by substitution (when the variable ` V ` has no
ENGOZPBCABUFMQAUFCAUFBRUFCRDFHJADNFOZPUFBCUGUFBCSALUAUBABUFMUCTUDUEMT $.
$}

${
$d x A $. $d x ph $.
vtocleg.1 $e |- ( x = A -> ph ) $.
$( Implicit substitution of a class for a setvar variable. (Contributed by
NM, 21-Jun-1993.) $)
vtocleg $p |- ( A e. V -> ph ) $=
( wcel cv wceq wex elisset exlimiv syl ) CDFBGCHZBIABCDJMABEKL $.
$}

${
$d x A $.
vtoclef.1 $e |- F/ x ph $.
vtoclef.2 $e |- A e. _V $.
vtoclef.3 $e |- ( x = A -> ph ) $.
$( Implicit substitution of a class for a setvar variable. (Contributed by
NM, 18-Aug-1993.) $)
vtoclef $p |- ph $=
( cv wceq wex isseti exlimi ax-mp ) BGCHZBIABCEJMABDFKL $.
$}

${
$d x A $.
vtoclf.1 $e |- F/ x ps $.
vtoclf.2 $e |- A e. _V $.
vtoclf.3 $e |- ( x = A -> ( ph <-> ps ) ) $.
vtoclf.4 $e |- ph $.
$( Implicit substitution of a class for a setvar variable. This is a
generalization of ~ chvar . (Contributed by NM, 30-Aug-1993.) $)
generalization of ~ chvar . (Contributed by NM, 30-Aug-1993.) (Proof
shortened by Wolf Lammen, 26-Jan-2025.) $)
vtoclf $p |- ps $=
( cv wceq mpbii vtoclef ) BCDEFCIDJABHGKL $.

$( Obsolete version of ~ vtoclf as of 26-Jan-2025. (Contributed by NM,
30-Aug-1993.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
vtoclfOLD $p |- ps $=
( cv wceq wi isseti biimpd eximii 19.36i mpg ) ABCABCECIDJZABKCCDFLQABGMN
OHP $.
$}
Expand Down Expand Up @@ -32956,8 +32983,8 @@ general is seen either by substitution (when the variable ` V ` has no
vtoclg1f.maj $e |- ( x = A -> ( ph <-> ps ) ) $.
vtoclg1f.min $e |- ph $.
$( Version of ~ vtoclgf with one nonfreeness hypothesis replaced with a
disjoint variable condition, thus avoiding dependency on ~ ax-11 and
~ ax-13 . (Contributed by BJ, 1-May-2019.) $)
disjoint variable condition, thus avoiding dependency on ~ ax-10 and
~ ax-11 . (Contributed by BJ, 1-May-2019.) $)
vtoclg1f $p |- ( A e. V -> ps ) $=
( wcel cv wceq wex elisset mpbii exlimi syl ) DEICJDKZCLBCDEMQBCFQABHGNOP
$.
Expand All @@ -32969,20 +32996,21 @@ general is seen either by substitution (when the variable ` V ` has no
vtoclg.2 $e |- ph $.
$( Implicit substitution of a class expression for a setvar variable.
(Contributed by NM, 17-Apr-1995.) Avoid ~ ax-12 . (Revised by SN,
20-Apr-2024.) $)
20-Apr-2024.) (Proof shortened by Wolf Lammen, 26-Jan-2025.) $)
vtoclg $p |- ( A e. V -> ps ) $=
( cv wceq mpbii vtocleg ) BCDECHDIABGFJK $.

$( Obsolete version of ~ vtoclg as of 26-Jan-2025. (Contributed by NM,
17-Apr-1995.) Avoid ~ ax-12 . (Revised by SN, 20-Apr-2024.)
(New usage is discouraged.) (Proof modification is discouraged.) $)
vtoclgOLD $p |- ( A e. V -> ps ) $=
( wcel cv wceq wex elisset mpbii exlimiv syl ) DEHCIDJZCKBCDELPBCPABGFMNO
$.
$}

${
$d x A $. $d x ps $.
vtoclgOLD.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
vtoclgOLD.2 $e |- ph $.
$( Obsolete version of ~ vtoclg as of 20-Apr-2024. (Contributed by NM,
17-Apr-1995.) (New usage is discouraged.)
(Proof modification is discouraged.) $)
vtoclgOLD $p |- ( A e. V -> ps ) $=
vtoclgOLDOLD $p |- ( A e. V -> ps ) $=
( nfv vtoclg1f ) ABCDEBCHFGI $.
$}

Expand Down Expand Up @@ -33222,38 +33250,28 @@ general is seen either by substitution (when the variable ` V ` has no
ULUM $.
$}

${
$d x A $. $d x ph $.
vtocleg.1 $e |- ( x = A -> ph ) $.
$( Implicit substitution of a class for a setvar variable. (Contributed by
NM, 21-Jun-1993.) $)
vtocleg $p |- ( A e. V -> ph ) $=
( wcel cv wceq wex elisset exlimiv syl ) CDFBGCHZBIABCDJMABEKL $.
$}

${
$d x A $.
$( Implicit substitution of a class for a setvar variable. (Closed theorem
version of ~ vtoclef .) (Contributed by NM, 7-Nov-2005.) (Revised by
Mario Carneiro, 11-Oct-2016.) $)
Mario Carneiro, 11-Oct-2016.) (Proof shortened by Wolf Lammen,
26-Jan-2025.) $)
vtoclegft $p |- ( ( A e. B /\ F/ x ph /\
A. x ( x = A -> ph ) ) -> ph ) $=
( wcel wnf cv wceq wi wal wa wb biidd ax-gen ceqsalt mp3an2 ancoms biimpd
3impia ) CDEZABFZBGCHZAIBJZATUAKUCAUATUCALZUAUBAALIZBJTUDUEBUBAMNAABCDOPQ
RS $.

$( Obsolete version of ~ vtoclegft as of 26-Jan-2025. (Contributed by NM,
7-Nov-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
vtoclegftOLD $p |- ( ( A e. B /\ F/ x ph /\
A. x ( x = A -> ph ) ) -> ph ) $=
( wcel wnf cv wceq wi wal w3a wex elisset mpan9 3adant2 wb 19.9t 3ad2ant2
exim mpbid ) CDEZABFZBGCHZAIBJZKABLZAUAUDUEUBUAUCBLUDUEBCDMUCABSNOUBUAUEA
PUDABQRT $.
$}

${
$d x A $.
vtoclef.1 $e |- F/ x ph $.
vtoclef.2 $e |- A e. _V $.
vtoclef.3 $e |- ( x = A -> ph ) $.
$( Implicit substitution of a class for a setvar variable. (Contributed by
NM, 18-Aug-1993.) $)
vtoclef $p |- ph $=
( cv wceq wex isseti exlimi ax-mp ) BGCHZBIABCEJMABDFKL $.
$}

${
$d x A $. $d x ph $.
vtocle.1 $e |- A e. _V $.
Expand Down Expand Up @@ -564868,6 +564886,19 @@ sides of the biconditional correlate (they are the same), if they exist at
( wnf wal wex weu wi wsb wmo wl-sb8et wl-sb8eut imbi12d moeu 3bitr4g ) ACDB
EZABFZABGZHABCIZCFZSCGZHABJSCJPQTRUAABCKABCLMABNSCNO $.

${
$d A y $. $d x y $.
wl-issetft.1 $e |- F/_ x A $.
$( A A closed form of ~ issetf . The proof here is a modification of a
subproof in ~ vtoclgft , where it could be used to shorten the proof.
(Contributed by Wolf Lammen, 25-Jan-2025.) $)
wl-issetft $p |- ( F/_ x A -> ( A e. _V <-> E. x x = A ) ) $=
( vy cvv wcel cv wceq wex wnfc isset wn wal nfnfc1 nfcvd nfeqd nfnd alnex
nfv id nfvd weq wb wi eqeq1 notbid a1i cbv2w 3bitr3g con4bid bitrid ) BEF
DGZBHZDIZABJZAGZBHZAIZDBKUOUNURUOUMLZDMUQLZAMUNLURLUOUSUTDAUODSABNUOUMAUO
AULBUOAULOUOTPQUOUTDUADAUBZUSUTUCUDUOVAUMUQULUPBUEUFUGUHUMDRUQARUIUJUK $.
$}

${
wl-axc11rc11.1 $e |- ( A. y y = x -> ( A. y y = x -> A. x y = x ) ) $.
wl-axc11rc11.2 $e |- ( A. x x = y -> ( A. x ph -> A. y ph ) ) $.
Expand Down
Loading