Home | Metamath
Proof ExplorerTheorem List
(p. 287 of 325)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-22374) |
Hilbert Space Explorer
(22375-23897) |
Users' Mathboxes
(23898-32447) |

Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|

Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunT1 28601 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunT1p1 28602 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunT21 28603 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun121 28604 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun121p1 28605 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun132 28606 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun132p1 28607 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | anabss7p1 28608 | A deduction unionizing a non-unionized collection of virtual hypotheses. This would have been named uun221 if the 0th permutation did not exist in set.mm as anabss7 795. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | un10 28609 | A unionizing deduction (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | un01 28610 | A unionizing deduction (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | un2122 28611 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun2131 28612 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun2131p1 28613 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunTT1 28614 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunTT1p1 28615 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunTT1p2 28616 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunT11 28617 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunT11p1 28618 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunT11p2 28619 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunT12 28620 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunT12p1 28621 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunT12p2 28622 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunT12p3 28623 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunT12p4 28624 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uunT12p5 28625 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun111 28626 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 3anidm12p1 28627 | A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1241 denotes the deduction which would have been named uun112 if it did not pre-exist in set.mm. This second permutation's name is based on this pre-existing name. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 3anidm12p2 28628 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun123 28629 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun123p1 28630 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun123p2 28631 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun123p3 28632 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun123p4 28633 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun2221 28634 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 30-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun2221p1 28635 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uun2221p2 28636 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 3impdirp1 28637 | A deduction unionizing a non-unionized collection of virtual hypotheses. 3impdir 1240 is ~? uun3132 and is in set.mm. 3impdirp1 28637 is ~? uun3132p1. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 3impcombi 28638 | A 1-hypothesis propositional calculus deduction (Contributed by Alan Sare, 25-Sep-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 3imp231 28639 | Importation inference. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

19.24.6 Theorems proved using virtual
deduction | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | trsspwALT 28640 | Virtual deduction proof of the left-to-right implication of dftr4 4267. A transitive class is a subset of its power class. This proof corresponds to the virtual deduction proof of dftr4 4267 without accumulating results. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | trsspwALT2 28641 | Virtual deduction proof of trsspwALT 28640. This proof is the same as the proof of trsspwALT 28640 except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A transitive class is a subset of its power class. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | trsspwALT3 28642 | Short predicate calculus proof of the left-to-right implication of dftr4 4267. A transitive class is a subset of its power class. This proof was constructed by applying Metamath's minimize command to the proof of trsspwALT2 28641, which is the virtual deduction proof trsspwALT 28640 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sspwtr 28643 | Virtual deduction proof of the right-to-left implication of dftr4 4267. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 28643 without accumulating results. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sspwtrALT 28644 | Virtual deduction proof of sspwtr 28643. This proof is the same as the proof of sspwtr 28643 except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A class which is a subclass of its power class is transitive. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sspwtrALT2 28645 | Short predicate calculus proof of the right-to-left implication of dftr4 4267. A class which is a subclass of its power class is transitive. This proof was constructed by applying Metamath's minimize command to the proof of sspwtrALT 28644, which is the virtual deduction proof sspwtr 28643 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pwtrVD 28646 | Virtual deduction proof of pwtr 4376. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pwtrrVD 28647 | Virtual deduction proof of pwtr 4376. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | snssiALTVD 28648 | Virtual deduction proof of snssiALT 28649. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | snssiALT 28649 | If a class is an element of another class, then its singleton is a subclass of that other class. Alternate proof of snssi 3902. This theorem was automatically generated from snssiALTVD 28648 using a translation program. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | snsslVD 28650 | Virtual deduction proof of snssl 28651. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | snssl 28651 | If a singleton is a subclass of another class, then the singleton's element is an element of that other class. This theorem is the right-to-left implication of the biconditional snss 3886. The proof of this theorem was automatically generated from snsslVD 28650 using a tools command file, translateMWO.cmd , by translating the proof into its non-virtual deduction form and minimizing it. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | snelpwrVD 28652 | Virtual deduction proof of snelpwi 4369. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | unipwrVD 28653 | Virtual deduction proof of unipwr 28654. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | unipwr 28654 | A class is a subclass of the union of its power class. This theorem is the right-to-left subclass lemma of unipw 4374. The proof of this theorem was automatically generated from unipwrVD 28653 using a tools command file , translateMWO.cmd , by translating the proof into its non-virtual deduction form and minimizing it. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sstrALT2VD 28655 | Virtual deduction proof of sstrALT2 28656. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sstrALT2 28656 |
Virtual deduction proof of sstr 3316, transitivity of subclasses, Theorem
6 of [Suppes] p. 23. This theorem was
automatically generated from
sstrALT2VD 28655 using the command file translate_{without}_overwriting.cmd .
It was not minimized because the automated minimization excluding
duplicates generates a minimized proof which, although not directly
containing any duplicates, indirectly contains a duplicate. That is,
the trace back of the minimized proof contains a duplicate. This is
undesirable because some step(s) of the minimized proof use the proven
theorem. (Contributed by Alan Sare, 11-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | suctrALT2VD 28657 | Virtual deduction proof of suctrALT2 28658. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | suctrALT2 28658 |
Virtual deduction proof of suctr 4624. The sucessor of a transitive class
is transitive. This proof was generated automatically from the virtual
deduction proof suctrALT2VD 28657 using the tools command file
translate_{without}_overwriting_{minimize}_excluding_{duplicates}.cmd .
(Contributed by Alan Sare, 11-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | elex2VD 28659* | Virtual deduction proof of elex2 2928. (Contributed by Alan Sare, 25-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | elex22VD 28660* | Virtual deduction proof of elex22 2927. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | eqsbc3rVD 28661* | Virtual deduction proof of eqsbc3r 3178. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | zfregs2VD 28662* | Virtual deduction proof of zfregs2 7625. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | tpid3gVD 28663 | Virtual deduction proof of tpid3g 3879. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | en3lplem1VD 28664* | Virtual deduction proof of en3lplem1 7626. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | en3lplem2VD 28665* | Virtual deduction proof of en3lplem2 7627. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | en3lpVD 28666 | Virtual deduction proof of en3lp 7628. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

19.24.7 Theorems proved using virtual deduction
with mmj2 assistance | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | simplbi2VD 28667 |
Virtual deduction proof of simplbi2 609. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 3ornot23VD 28668 |
Virtual deduction proof of 3ornot23 28302. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | orbi1rVD 28669 |
Virtual deduction proof of orbi1r 28303. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bitr3VD 28670 |
Virtual deduction proof of bitr3 28304. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 3orbi123VD 28671 |
Virtual deduction proof of 3orbi123 28305. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sbc3orgVD 28672 |
Virtual deduction proof of sbc3org 28327. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 19.21a3con13vVD 28673* |
Virtual deduction proof of alrim3con13v 28328. The following user's
proof is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | exbirVD 28674 |
Virtual deduction proof of exbir 1371. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | exbiriVD 28675 |
Virtual deduction proof of exbiri 606. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | rspsbc2VD 28676* |
Virtual deduction proof of rspsbc2 28329. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 3impexpVD 28677 |
Virtual deduction proof of 3impexp 1372. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 3impexpbicomVD 28678 |
Virtual deduction proof of 3impexpbicom 1373. The following user's proof
is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 3impexpbicomiVD 28679 |
Virtual deduction proof of 3impexpbicomi 1374. The following user's proof
is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sbcoreleleqVD 28680* |
Virtual deduction proof of sbcoreleleq 28330. The following user's proof
is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | hbra2VD 28681* |
Virtual deduction proof of nfra2 2720. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | tratrbVD 28682* |
Virtual deduction proof of tratrb 28331. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 3ax5VD 28683 |
Virtual deduction proof of 3ax5 28332. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl5impVD 28684 |
Virtual deduction proof of syl5imp 28306. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | idiVD 28685 |
Virtual deduction proof of idi 2. The following user's
proof is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ancomsimpVD 28686 |
Closed form of ancoms 440. The following user's proof is completed by
invoking mmj2's unify command and using mmj2's StepSelector to pick all
remaining steps of the Metamath proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ssralv2VD 28687* |
Quantification restricted to a subclass for two quantifiers. ssralv 3367
for two quantifiers. The following User's Proof is a Virtual Deduction
proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. ssralv2 28326 is ssralv2VD 28687 without
virtual deductions and was automatically derived from ssralv2VD 28687.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ordelordALTVD 28688 |
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36. This is an alternate proof of ordelord 4563 using
the Axiom of Regularity indirectly through dford2 7531. dford2 is a
weaker definition of ordinal number. Given the Axiom of Regularity, it
need not be assumed that because this is inferred by the
Axiom of Regularity. The following User's Proof is a Virtual Deduction
proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. ordelordALT 28333 is ordelordALTVD 28688
without virtual deductions and was automatically derived from
ordelordALTVD 28688 using the tools program
translate..without..overwriting.cmd and Metamath's minimize command.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | equncomVD 28689 |
If a class equals the union of two other classes, then it equals the
union of those two classes commuted. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. equncom 3452 is equncomVD 28689 without
virtual deductions and was automatically derived from equncomVD 28689.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | equncomiVD 28690 |
Inference form of equncom 3452. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. equncomi 3453 is equncomiVD 28690 without
virtual deductions and was automatically derived from equncomiVD 28690.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sucidALTVD 28691 |
A set belongs to its successor. Alternate proof of sucid 4620.
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. sucidALT 28692 is sucidALTVD 28691
without virtual deductions and was automatically derived from
sucidALTVD 28691. This proof illustrates that
completeusersproof.cmd will generate a Metamath proof from any
User's Proof which is "conventional" in the sense that no step
is a virtual deduction, provided that all necessary unification
theorems and transformation deductions are in set.mm.
completeusersproof.cmd automatically converts such a
conventional proof into a Virtual Deduction proof for which each
step happens to be a 0-virtual hypothesis virtual deduction.
The user does not need to search for reference theorem labels or
deduction labels nor does he(she) need to use theorems and
deductions which unify with reference theorems and deductions in
set.mm. All that is necessary is that each theorem or deduction
of the User's Proof unifies with some reference theorem or
deduction in set.mm or is a semantic variation of some theorem
or deduction which unifies with some reference theorem or
deduction in set.mm. The definition of "semantic variation" has
not been precisely defined. If it is obvious that a theorem or
deduction has the same meaning as another theorem or deduction,
then it is a semantic variation of the latter theorem or
deduction. For example, step 4 of the User's Proof is a
semantic variation of the definition (axiom)
, which unifies with df-suc 4547, a
reference definition (axiom) in set.mm. Also, a theorem or
deduction is said to be a semantic variation of another
theorem or deduction if it is obvious upon cursory inspection
that it has the same meaning as a weaker form of the latter
theorem or deduction. For example, the deduction
infers is a
semantic variation of the theorem
, which unifies with
the set.mm reference definition (axiom) dford2 7531.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sucidALT 28692 |
A set belongs to its successor. This proof was automatically derived
from sucidALTVD 28691 using translate_{without}_overwriting.cmd and
minimizing. (Contributed by Alan Sare, 18-Feb-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sucidVD 28693 |
A set belongs to its successor. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools
program completeusersproof.cmd, which invokes Mel O'Cat's mmj2
and Norm Megill's Metamath Proof Assistant. sucid 4620 is
sucidVD 28693 without virtual deductions and was automatically
derived from sucidVD 28693.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | imbi12VD 28694 |
Implication form of imbi12i 317. The following User's Proof is a Virtual
Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi12 28314
is imbi12VD 28694 without virtual deductions and was automatically derived
from imbi12VD 28694.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | imbi13VD 28695 |
Join three logical equivalences to form equivalence of implications. The
following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi13 28315
is imbi13VD 28695 without virtual deductions and was automatically derived
from imbi13VD 28695.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sbcim2gVD 28696 |
Distribution of class substitution over a left-nested implication.
Similar
to sbcimg 3162. The following User's Proof is a Virtual Deduction proof
completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcim2g 28334
is sbcim2gVD 28696 without virtual deductions and was automatically derived
from sbcim2gVD 28696.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sbcbiVD 28697 |
Implication form of sbcbiiOLD 3177. The following User's Proof is a
Virtual
Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcbi 28335
is sbcbiVD 28697 without virtual deductions and was automatically derived
from sbcbiVD 28697.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | trsbcVD 28698* |
Formula-building inference rule for class substitution, substituting a
class
variable for the set variable of the transitivity predicate. The
following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trsbc 28336
is trsbcVD 28698 without virtual deductions and was automatically derived
from trsbcVD 28698.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | truniALTVD 28699* |
The union of a class of transitive sets is transitive. The following
User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. truniALT 28337
is truniALTVD 28699 without virtual deductions and was automatically derived
from truniALTVD 28699.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ee33VD 28700 |
Non-virtual deduction form of e33 28555. The following User's Proof is a
Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. ee33 28316
is ee33VD 28700 without virtual deductions and was automatically derived
from ee33VD 28700.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |