Theorem lrrecpred

Description: Finally, we calculate the value of the predecessor class over R . (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypothesis	lrrec.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
Assertion	lrrecpred	⊢ ( 𝐴 ∈ No → Pred ( 𝑅 , No , 𝐴 ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lrrec.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
2		dfpred3g	⊢ ( 𝐴 ∈ No → Pred ( 𝑅 , No , 𝐴 ) = { 𝑏 ∈ No ∣ 𝑏 𝑅 𝐴 } )
3	1	lrrecval	⊢ ( ( 𝑏 ∈ No ∧ 𝐴 ∈ No ) → ( 𝑏 𝑅 𝐴 ↔ 𝑏 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) )
4	3	ancoms	⊢ ( ( 𝐴 ∈ No ∧ 𝑏 ∈ No ) → ( 𝑏 𝑅 𝐴 ↔ 𝑏 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) )
5	4	rabbidva	⊢ ( 𝐴 ∈ No → { 𝑏 ∈ No ∣ 𝑏 𝑅 𝐴 } = { 𝑏 ∈ No ∣ 𝑏 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) } )
6		dfrab2	⊢ { 𝑏 ∈ No ∣ 𝑏 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) } = ( { 𝑏 ∣ 𝑏 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) } ∩ No )
7		abid2	⊢ { 𝑏 ∣ 𝑏 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) } = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) )
8	7	ineq1i	⊢ ( { 𝑏 ∣ 𝑏 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) } ∩ No ) = ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∩ No )
9	6 8	eqtri	⊢ { 𝑏 ∈ No ∣ 𝑏 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) } = ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∩ No )
10	5 9	eqtrdi	⊢ ( 𝐴 ∈ No → { 𝑏 ∈ No ∣ 𝑏 𝑅 𝐴 } = ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∩ No ) )
11		leftssold	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) )
12		bdayelon	⊢ ( bday ‘ 𝐴 ) ∈ On
13		oldf	⊢ O : On ⟶ 𝒫 No
14	13	ffvelrni	⊢ ( ( bday ‘ 𝐴 ) ∈ On → ( O ‘ ( bday ‘ 𝐴 ) ) ∈ 𝒫 No )
15	14	elpwid	⊢ ( ( bday ‘ 𝐴 ) ∈ On → ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No )
16	12 15	ax-mp	⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No
17	11 16	sstrdi	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ⊆ No )
18		rightssold	⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) )
19	18 16	sstrdi	⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) ⊆ No )
20	17 19	unssd	⊢ ( 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ⊆ No )
21		df-ss	⊢ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ⊆ No ↔ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∩ No ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
22	20 21	sylib	⊢ ( 𝐴 ∈ No → ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∩ No ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
23	2 10 22	3eqtrd	⊢ ( 𝐴 ∈ No → Pred ( 𝑅 , No , 𝐴 ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )