Theorem noxpordfr

Description: Next we establish the foundedness 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	noxpordfr	⊢ 𝑆 Fr ( No × No )

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	1	lrrecfr	⊢ 𝑅 Fr No
4	3	a1i	⊢ ( ⊤ → 𝑅 Fr No )
5	2 4 4	frxp2	⊢ ( ⊤ → 𝑆 Fr ( No × No ) )
6	5	mptru	⊢ 𝑆 Fr ( No × No )