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 ⊢ R = x y | x ∈ L ⁡ y ∪ R ⁡ y
Assertion lrrecpo ⊢ R Po No

Proof

Step Hyp Ref Expression
1 lrrec.1 ⊢ R = x y | x ∈ L ⁡ y ∪ R ⁡ y
2 bdayelon ⊢ bday ⁡ a ∈ On
3 2 onirri ⊢ ¬ bday ⁡ a ∈ bday ⁡ a
4 1 lrrecval2 ⊢ a ∈ No ∧ a ∈ No → a R a ↔ bday ⁡ a ∈ bday ⁡ a
5 4 anidms ⊢ a ∈ No → a R a ↔ bday ⁡ a ∈ bday ⁡ a
6 3 5 mtbiri ⊢ a ∈ No → ¬ a R a
7 6 adantl ⊢ ⊤ ∧ a ∈ No → ¬ a R a
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 → a R b ↔ bday ⁡ a ∈ bday ⁡ b
12 11 3adant3 ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → a R b ↔ bday ⁡ a ∈ bday ⁡ b
13 1 lrrecval2 ⊢ b ∈ No ∧ c ∈ No → b R c ↔ bday ⁡ b ∈ bday ⁡ c
14 13 3adant1 ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → b R c ↔ bday ⁡ b ∈ bday ⁡ c
15 12 14 anbi12d ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → a R b ∧ b R c ↔ bday ⁡ a ∈ bday ⁡ b ∧ bday ⁡ b ∈ bday ⁡ c
16 1 lrrecval2 ⊢ a ∈ No ∧ c ∈ No → a R c ↔ bday ⁡ a ∈ bday ⁡ c
17 16 3adant2 ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → a R c ↔ bday ⁡ a ∈ bday ⁡ c
18 15 17 imbi12d ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → a R b ∧ b R c → a R c ↔ bday ⁡ a ∈ bday ⁡ b ∧ bday ⁡ b ∈ bday ⁡ c → bday ⁡ a ∈ bday ⁡ c
19 10 18 mpbiri ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → a R b ∧ b R c → a R c
20 19 adantl ⊢ ⊤ ∧ a ∈ No ∧ b ∈ No ∧ c ∈ No → a R b ∧ b R c → a R c
21 7 20 ispod ⊢ ⊤ → R Po No
22 21 mptru ⊢ R Po No