Theorem nfso

Description: Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015)

	Ref	Expression
Hypotheses	nfpo.r	⊢ Ⅎ 𝑥 𝑅
	nfpo.a	⊢ Ⅎ 𝑥 𝐴
Assertion	nfso	⊢ Ⅎ 𝑥 𝑅 Or 𝐴

Proof

Step	Hyp	Ref	Expression
1		nfpo.r	⊢ Ⅎ 𝑥 𝑅
2		nfpo.a	⊢ Ⅎ 𝑥 𝐴
3		df-so	⊢ ( 𝑅 Or 𝐴 ↔ ( 𝑅 Po 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑅 𝑎 ) ) )
4	1 2	nfpo	⊢ Ⅎ 𝑥 𝑅 Po 𝐴
5		nfcv	⊢ Ⅎ 𝑥 𝑎
6		nfcv	⊢ Ⅎ 𝑥 𝑏
7	5 1 6	nfbr	⊢ Ⅎ 𝑥 𝑎 𝑅 𝑏
8		nfv	⊢ Ⅎ 𝑥 𝑎 = 𝑏
9	6 1 5	nfbr	⊢ Ⅎ 𝑥 𝑏 𝑅 𝑎
10	7 8 9	nf3or	⊢ Ⅎ 𝑥 ( 𝑎 𝑅 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑅 𝑎 )
11	2 10	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑅 𝑎 )
12	2 11	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑅 𝑎 )
13	4 12	nfan	⊢ Ⅎ 𝑥 ( 𝑅 Po 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑅 𝑎 ) )
14	3 13	nfxfr	⊢ Ⅎ 𝑥 𝑅 Or 𝐴