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 = (/) )