Metamath Proof Explorer

Theorem oiiniseg

Description: ran F is an initial segment of A under the well-order R . (Contributed by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypothesis oicl.1 ⊢F=OrdIsoRA
Assertion oiiniseg ⊢RWeA∧RSeA∧N∈A∧M∈dom⁡F→F⁡MRN∨N∈ran⁡F

Proof

Step Hyp Ref Expression
1 oicl.1 ⊢F=OrdIsoRA
2 eqid ⊢recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
3 eqid ⊢w∈A|∀j∈ran⁡hjRw=w∈A|∀j∈ran⁡hjRw
4 eqid ⊢h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv=h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
5 2 3 4 ordtypecbv ⊢recs⁡f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRs=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
6 eqid ⊢x∈On|∃t∈A∀z∈recs⁡f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRsxzRt=x∈On|∃t∈A∀z∈recs⁡f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRsxzRt
7 simpl ⊢RWeA∧RSeA→RWeA
8 simpr ⊢RWeA∧RSeA→RSeA
9 5 3 4 6 1 7 8 ordtypelem7 ⊢RWeA∧RSeA∧N∈A∧M∈dom⁡F→F⁡MRN∨N∈ran⁡F
10 9 anasss ⊢RWeA∧RSeA∧N∈A∧M∈dom⁡F→F⁡MRN∨N∈ran⁡F