This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oi0

Description: Definition of the ordinal isomorphism when its arguments are not meaningful. (Contributed by Mario Carneiro, 25-Jun-2015)

Ref Expression
Hypothesis oicl.1 
|- F = OrdIso ( R , A )
Assertion oi0 
|- ( -. ( R We A /\ R Se A ) -> F = (/) )

Proof

Step Hyp Ref Expression
1 oicl.1 
 |-  F = OrdIso ( R , A )
2 df-oi 
 |-  OrdIso ( R , A ) = if ( ( R We A /\ R Se A ) , ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) |` { x e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t } ) , (/) )
3 1 2 eqtri 
 |-  F = if ( ( R We A /\ R Se A ) , ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) |` { x e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t } ) , (/) )
4 iffalse 
 |-  ( -. ( R We A /\ R Se A ) -> if ( ( R We A /\ R Se A ) , ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) |` { x e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t } ) , (/) ) = (/) )
5 3 4 eqtrid 
 |-  ( -. ( R We A /\ R Se A ) -> F = (/) )