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⁡hjRw
ordtypelem.3 ⊢G=h∈V⟼ιv∈C|∀u∈C¬uRv
Assertion ordtypecbv ⊢recs⁡f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRs=F

Proof

Step Hyp Ref Expression
1 ordtypelem.1 ⊢F=recs⁡G
2 ordtypelem.2 ⊢C=w∈A|∀j∈ran⁡hjRw
3 ordtypelem.3 ⊢G=h∈V⟼ιv∈C|∀u∈C¬uRv
4 breq1 ⊢u=r→uRv↔rRv
5 4 notbid ⊢u=r→¬uRv↔¬rRv
6 5 cbvralvw ⊢∀u∈C¬uRv↔∀r∈C¬rRv
7 breq2 ⊢v=s→rRv↔rRs
8 7 notbid ⊢v=s→¬rRv↔¬rRs
9 8 ralbidv ⊢v=s→∀r∈C¬rRv↔∀r∈C¬rRs
10 6 9 bitrid ⊢v=s→∀u∈C¬uRv↔∀r∈C¬rRs
11 10 cbvriotavw ⊢ιv∈C|∀u∈C¬uRv=ιs∈C|∀r∈C¬rRs
12 breq1 ⊢j=i→jRw↔iRw
13 12 cbvralvw ⊢∀j∈ran⁡hjRw↔∀i∈ran⁡hiRw
14 breq2 ⊢w=y→iRw↔iRy
15 14 ralbidv ⊢w=y→∀i∈ran⁡hiRw↔∀i∈ran⁡hiRy
16 13 15 bitrid ⊢w=y→∀j∈ran⁡hjRw↔∀i∈ran⁡hiRy
17 16 cbvrabv ⊢w∈A|∀j∈ran⁡hjRw=y∈A|∀i∈ran⁡hiRy
18 2 17 eqtri ⊢C=y∈A|∀i∈ran⁡hiRy
19 rneq ⊢h=f→ran⁡h=ran⁡f
20 19 raleqdv ⊢h=f→∀i∈ran⁡hiRy↔∀i∈ran⁡fiRy
21 20 rabbidv ⊢h=f→y∈A|∀i∈ran⁡hiRy=y∈A|∀i∈ran⁡fiRy
22 18 21 eqtrid ⊢h=f→C=y∈A|∀i∈ran⁡fiRy
23 22 raleqdv ⊢h=f→∀r∈C¬rRs↔∀r∈y∈A|∀i∈ran⁡fiRy¬rRs
24 22 23 riotaeqbidv ⊢h=f→ιs∈C|∀r∈C¬rRs=ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRs
25 11 24 eqtrid ⊢h=f→ιv∈C|∀u∈C¬uRv=ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRs
26 25 cbvmptv ⊢h∈V⟼ιv∈C|∀u∈C¬uRv=f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRs
27 3 26 eqtri ⊢G=f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRs
28 recseq ⊢G=f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRs→recs⁡G=recs⁡f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRs
29 27 28 ax-mp ⊢recs⁡G=recs⁡f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRs
30 1 29 eqtr2i ⊢recs⁡f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRs=F