Theorem noxpordpred

Description: Next we calculate the predecessor class of the relationship. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypotheses	noxpord.1	⊢ 𝑅 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) }
	noxpord.2	⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑅 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
Assertion	noxpordpred	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → Pred ( 𝑆 , ( No × No ) , ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		noxpord.1	⊢ 𝑅 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) }
2		noxpord.2	⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑅 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
3	2	xpord2pred	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → Pred ( 𝑆 , ( No × No ) , ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ( Pred ( 𝑅 , No , 𝐴 ) ∪ { 𝐴 } ) × ( Pred ( 𝑅 , No , 𝐵 ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
4	1	lrrecpred	⊢ ( 𝐴 ∈ No → Pred ( 𝑅 , No , 𝐴 ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
5	4	adantr	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → Pred ( 𝑅 , No , 𝐴 ) = ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
6	5	uneq1d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( Pred ( 𝑅 , No , 𝐴 ) ∪ { 𝐴 } ) = ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
7	1	lrrecpred	⊢ ( 𝐵 ∈ No → Pred ( 𝑅 , No , 𝐵 ) = ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
8	7	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → Pred ( 𝑅 , No , 𝐵 ) = ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
9	8	uneq1d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( Pred ( 𝑅 , No , 𝐵 ) ∪ { 𝐵 } ) = ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
10	6 9	xpeq12d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( Pred ( 𝑅 , No , 𝐴 ) ∪ { 𝐴 } ) × ( Pred ( 𝑅 , No , 𝐵 ) ∪ { 𝐵 } ) ) = ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) )
11	10	difeq1d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( ( Pred ( 𝑅 , No , 𝐴 ) ∪ { 𝐴 } ) × ( Pred ( 𝑅 , No , 𝐵 ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
12	3 11	eqtrd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → Pred ( 𝑆 , ( No × No ) , ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )