Theorem fin2inf 4634

Description: This (useless) theorem, which was proved without the Axiom of Infinity, demonstrates an artifact of our definition of strict dominance, which is meaningful only when its arguments exist. In particular, the antecedent cannot be satisfied unless om exists.

Assertion

Ref	Expression
fin2inf	|- (A ~< om -> om e. V)

Proof of Theorem fin2inf

Step	Hyp	Ref	Expression
1		sdomex 4560	. 2 |- (A ~< om -> (A e. V /\ om e. V))
2	1	pm3.27d 323	1 |- (A ~< om -> om e. V)

Syntax hints:   -> wi 3   e. wcel 990  Vcvv 1849   class class class wbr 2669  omcom 3192   ~< csdm 4453

This theorem is referenced by:  unfi2 4639  unifi2 4643

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-9 997  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832  ax-un 2920

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-rex 1688  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-id 2889  df-xp 3239  df-rel 3240  df-cnv 3241  df-co 3242  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fun 3247  df-fn 3248  df-f 3249  df-f1 3250  df-fo 3251  df-f1o 3252  df-en 4455  df-dom 4456  df-sdom 4457

Copyright terms: Public domain