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	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
Assertion	lrrecpo	⊢ 𝑅 Po No

Proof

Step	Hyp	Ref	Expression
1		lrrec.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
2		bdayelon	⊢ ( bday ‘ 𝑎 ) ∈ On
3	2	onirri	⊢ ¬ ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑎 )
4	1	lrrecval2	⊢ ( ( 𝑎 ∈ No ∧ 𝑎 ∈ No ) → ( 𝑎 𝑅 𝑎 ↔ ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑎 ) ) )
5	4	anidms	⊢ ( 𝑎 ∈ No → ( 𝑎 𝑅 𝑎 ↔ ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑎 ) ) )
6	3 5	mtbiri	⊢ ( 𝑎 ∈ No → ¬ 𝑎 𝑅 𝑎 )
7	6	adantl	⊢ ( ( ⊤ ∧ 𝑎 ∈ No ) → ¬ 𝑎 𝑅 𝑎 )
8		bdayelon	⊢ ( bday ‘ 𝑐 ) ∈ On
9		ontr1	⊢ ( ( bday ‘ 𝑐 ) ∈ On → ( ( ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑏 ) ∧ ( bday ‘ 𝑏 ) ∈ ( bday ‘ 𝑐 ) ) → ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑐 ) ) )
10	8 9	ax-mp	⊢ ( ( ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑏 ) ∧ ( bday ‘ 𝑏 ) ∈ ( bday ‘ 𝑐 ) ) → ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑐 ) )
11	1	lrrecval2	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ) → ( 𝑎 𝑅 𝑏 ↔ ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑏 ) ) )
12	11	3adant3	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( 𝑎 𝑅 𝑏 ↔ ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑏 ) ) )
13	1	lrrecval2	⊢ ( ( 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( 𝑏 𝑅 𝑐 ↔ ( bday ‘ 𝑏 ) ∈ ( bday ‘ 𝑐 ) ) )
14	13	3adant1	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( 𝑏 𝑅 𝑐 ↔ ( bday ‘ 𝑏 ) ∈ ( bday ‘ 𝑐 ) ) )
15	12 14	anbi12d	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ( 𝑎 𝑅 𝑏 ∧ 𝑏 𝑅 𝑐 ) ↔ ( ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑏 ) ∧ ( bday ‘ 𝑏 ) ∈ ( bday ‘ 𝑐 ) ) ) )
16	1	lrrecval2	⊢ ( ( 𝑎 ∈ No ∧ 𝑐 ∈ No ) → ( 𝑎 𝑅 𝑐 ↔ ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑐 ) ) )
17	16	3adant2	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( 𝑎 𝑅 𝑐 ↔ ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑐 ) ) )
18	15 17	imbi12d	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ( ( 𝑎 𝑅 𝑏 ∧ 𝑏 𝑅 𝑐 ) → 𝑎 𝑅 𝑐 ) ↔ ( ( ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑏 ) ∧ ( bday ‘ 𝑏 ) ∈ ( bday ‘ 𝑐 ) ) → ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝑐 ) ) ) )
19	10 18	mpbiri	⊢ ( ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → ( ( 𝑎 𝑅 𝑏 ∧ 𝑏 𝑅 𝑐 ) → 𝑎 𝑅 𝑐 ) )
20	19	adantl	⊢ ( ( ⊤ ∧ ( 𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) ) → ( ( 𝑎 𝑅 𝑏 ∧ 𝑏 𝑅 𝑐 ) → 𝑎 𝑅 𝑐 ) )
21	7 20	ispod	⊢ ( ⊤ → 𝑅 Po No )
22	21	mptru	⊢ 𝑅 Po No