Metamath Proof Explorer

Theorem lrrecpo

Description: Now, we establish that R is a partial ordering on No . (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypothesis lrrec.1 No typesetting found for |- R = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode |-
Assertion lrrecpo ⊢RPoNo

Proof

Step Hyp Ref Expression
1 lrrec.1 Could not format R = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } : No typesetting found for |- R = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode |-
2 bdayelon ⊢bday⁡a∈On
3 2 onirri ⊢¬bday⁡a∈bday⁡a
4 1 lrrecval2 ⊢a∈No∧a∈No→aRa↔bday⁡a∈bday⁡a
5 4 anidms ⊢a∈No→aRa↔bday⁡a∈bday⁡a
6 3 5 mtbiri ⊢a∈No→¬aRa
7 6 adantl ⊢⊤∧a∈No→¬aRa
8 bdayelon ⊢bday⁡c∈On
9 ontr1 ⊢bday⁡c∈On→bday⁡a∈bday⁡b∧bday⁡b∈bday⁡c→bday⁡a∈bday⁡c
10 8 9 ax-mp ⊢bday⁡a∈bday⁡b∧bday⁡b∈bday⁡c→bday⁡a∈bday⁡c
11 1 lrrecval2 ⊢a∈No∧b∈No→aRb↔bday⁡a∈bday⁡b
12 11 3adant3 ⊢a∈No∧b∈No∧c∈No→aRb↔bday⁡a∈bday⁡b
13 1 lrrecval2 ⊢b∈No∧c∈No→bRc↔bday⁡b∈bday⁡c
14 13 3adant1 ⊢a∈No∧b∈No∧c∈No→bRc↔bday⁡b∈bday⁡c
15 12 14 anbi12d ⊢a∈No∧b∈No∧c∈No→aRb∧bRc↔bday⁡a∈bday⁡b∧bday⁡b∈bday⁡c
16 1 lrrecval2 ⊢a∈No∧c∈No→aRc↔bday⁡a∈bday⁡c
17 16 3adant2 ⊢a∈No∧b∈No∧c∈No→aRc↔bday⁡a∈bday⁡c
18 15 17 imbi12d ⊢a∈No∧b∈No∧c∈No→aRb∧bRc→aRc↔bday⁡a∈bday⁡b∧bday⁡b∈bday⁡c→bday⁡a∈bday⁡c
19 10 18 mpbiri ⊢a∈No∧b∈No∧c∈No→aRb∧bRc→aRc
20 19 adantl ⊢⊤∧a∈No∧b∈No∧c∈No→aRb∧bRc→aRc
21 7 20 ispod ⊢⊤→RPoNo
22 21 mptru ⊢RPoNo