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 V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v x On | t A z recs h V ι v w A | j ran h j R w | u w A | j 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 V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v x On | t A z recs h V ι v w A | j ran h j R w | u w A | j 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 V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v x On | t A z recs h V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v x z R t =
5 3 4 eqtrid ¬ R We A R Se A F =