Metamath Proof Explorer


Theorem dfoi

Description: Rewrite df-oi with abbreviations. (Contributed by Mario Carneiro, 24-Jun-2015)

Ref Expression
Hypotheses dfoi.1 C = w A | j ran h j R w
dfoi.2 G = h V ι v C | u C ¬ u R v
dfoi.3 F = recs G
Assertion dfoi OrdIso R A = if R We A R Se A F x On | t A z F x z R t

Proof

Step Hyp Ref Expression
1 dfoi.1 C = w A | j ran h j R w
2 dfoi.2 G = h V ι v C | u C ¬ u R v
3 dfoi.3 F = recs G
4 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
5 1 a1i h V C = w A | j ran h j R w
6 5 raleqdv h V u C ¬ u R v u w A | j ran h j R w ¬ u R v
7 5 6 riotaeqbidv h V ι v C | u C ¬ u R v = ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v
8 7 mpteq2ia h V ι v C | u C ¬ u R v = h V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v
9 2 8 eqtri G = h V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v
10 recseq G = h V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v recs G = recs h V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v
11 9 10 ax-mp recs G = recs h V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v
12 3 11 eqtri F = recs h V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v
13 12 imaeq1i F x = 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
14 13 raleqi z F x z R t 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
15 14 rexbii t A z F x z R t 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
16 15 rabbii x On | t A z F x z R t = 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
17 12 16 reseq12i F x On | t A z F x z R t = 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
18 ifeq1 F x On | t A z F x z R t = 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 if R We A R Se A F x On | t A z F x z R t = 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
19 17 18 ax-mp if R We A R Se A F x On | t A z F x z R t = 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
20 4 19 eqtr4i OrdIso R A = if R We A R Se A F x On | t A z F x z R t