Metamath Proof Explorer


Theorem ordtypecbv

Description: Lemma for ordtype . (Contributed by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses ordtypelem.1 F = recs G
ordtypelem.2 C = w A | j ran h j R w
ordtypelem.3 G = h V ι v C | u C ¬ u R v
Assertion ordtypecbv recs f V ι s y A | i ran f i R y | r y A | i ran f i R y ¬ r R s = F

Proof

Step Hyp Ref Expression
1 ordtypelem.1 F = recs G
2 ordtypelem.2 C = w A | j ran h j R w
3 ordtypelem.3 G = h V ι v C | u C ¬ u R v
4 breq1 u = r u R v r R v
5 4 notbid u = r ¬ u R v ¬ r R v
6 5 cbvralvw u C ¬ u R v r C ¬ r R v
7 breq2 v = s r R v r R s
8 7 notbid v = s ¬ r R v ¬ r R s
9 8 ralbidv v = s r C ¬ r R v r C ¬ r R s
10 6 9 syl5bb v = s u C ¬ u R v r C ¬ r R s
11 10 cbvriotavw ι v C | u C ¬ u R v = ι s C | r C ¬ r R s
12 breq1 j = i j R w i R w
13 12 cbvralvw j ran h j R w i ran h i R w
14 breq2 w = y i R w i R y
15 14 ralbidv w = y i ran h i R w i ran h i R y
16 13 15 syl5bb w = y j ran h j R w i ran h i R y
17 16 cbvrabv w A | j ran h j R w = y A | i ran h i R y
18 2 17 eqtri C = y A | i ran h i R y
19 rneq h = f ran h = ran f
20 19 raleqdv h = f i ran h i R y i ran f i R y
21 20 rabbidv h = f y A | i ran h i R y = y A | i ran f i R y
22 18 21 eqtrid h = f C = y A | i ran f i R y
23 22 raleqdv h = f r C ¬ r R s r y A | i ran f i R y ¬ r R s
24 22 23 riotaeqbidv h = f ι s C | r C ¬ r R s = ι s y A | i ran f i R y | r y A | i ran f i R y ¬ r R s
25 11 24 eqtrid h = f ι v C | u C ¬ u R v = ι s y A | i ran f i R y | r y A | i ran f i R y ¬ r R s
26 25 cbvmptv h V ι v C | u C ¬ u R v = f V ι s y A | i ran f i R y | r y A | i ran f i R y ¬ r R s
27 3 26 eqtri G = f V ι s y A | i ran f i R y | r y A | i ran f i R y ¬ r R s
28 recseq G = f V ι s y A | i ran f i R y | r y A | i ran f i R y ¬ r R s recs G = recs f V ι s y A | i ran f i R y | r y A | i ran f i R y ¬ r R s
29 27 28 ax-mp recs G = recs f V ι s y A | i ran f i R y | r y A | i ran f i R y ¬ r R s
30 1 29 eqtr2i recs f V ι s y A | i ran f i R y | r y A | i ran f i R y ¬ r R s = F