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		leftssno	⊢ ( L ‘ 𝐴 ) ⊆ No
12	11	a1i	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ⊆ No )
13		rightssno	⊢ ( R ‘ 𝐴 ) ⊆ No
14	13	a1i	⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) ⊆ No )
15	12 14	unssd	⊢ ( 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ⊆ No )
16		dfss2	⊢ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ⊆ No ↔ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∩ No ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
17	15 16	sylib	⊢ ( 𝐴 ∈ No → ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∩ No ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
18	2 10 17	3eqtrd	⊢ ( 𝐴 ∈ No → Pred ( 𝑅 , No , 𝐴 ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )