Metamath Proof Explorer


Theorem omsindsOLD

Description: Obsolete version of omsinds as of 16-Oct-2024. (Contributed by Scott Fenton, 17-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses omsinds.1
|- ( x = y -> ( ph <-> ps ) )
omsinds.2
|- ( x = A -> ( ph <-> ch ) )
omsinds.3
|- ( x e. _om -> ( A. y e. x ps -> ph ) )
Assertion omsindsOLD
|- ( A e. _om -> ch )

Proof

Step Hyp Ref Expression
1 omsinds.1
 |-  ( x = y -> ( ph <-> ps ) )
2 omsinds.2
 |-  ( x = A -> ( ph <-> ch ) )
3 omsinds.3
 |-  ( x e. _om -> ( A. y e. x ps -> ph ) )
4 omsson
 |-  _om C_ On
5 epweon
 |-  _E We On
6 wess
 |-  ( _om C_ On -> ( _E We On -> _E We _om ) )
7 4 5 6 mp2
 |-  _E We _om
8 epse
 |-  _E Se _om
9 predep
 |-  ( x e. _om -> Pred ( _E , _om , x ) = ( _om i^i x ) )
10 ordom
 |-  Ord _om
11 ordtr
 |-  ( Ord _om -> Tr _om )
12 trss
 |-  ( Tr _om -> ( x e. _om -> x C_ _om ) )
13 10 11 12 mp2b
 |-  ( x e. _om -> x C_ _om )
14 sseqin2
 |-  ( x C_ _om <-> ( _om i^i x ) = x )
15 13 14 sylib
 |-  ( x e. _om -> ( _om i^i x ) = x )
16 9 15 eqtrd
 |-  ( x e. _om -> Pred ( _E , _om , x ) = x )
17 16 raleqdv
 |-  ( x e. _om -> ( A. y e. Pred ( _E , _om , x ) ps <-> A. y e. x ps ) )
18 17 3 sylbid
 |-  ( x e. _om -> ( A. y e. Pred ( _E , _om , x ) ps -> ph ) )
19 7 8 1 2 18 wfis3
 |-  ( A e. _om -> ch )