Theorem nfso

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

	Ref	Expression
Hypotheses	nfpo.r	|- F/_ x R
	nfpo.a	|- F/_ x A
Assertion	nfso	|- F/ x R Or A

Proof

Step	Hyp	Ref	Expression
1		nfpo.r	|- F/_ x R
2		nfpo.a	|- F/_ x A
3		df-so	|- ( R Or A <-> ( R Po A /\ A. a e. A A. b e. A ( a R b \/ a = b \/ b R a ) ) )
4	1 2	nfpo	|- F/ x R Po A
5		nfcv	|- F/_ x a
6		nfcv	|- F/_ x b
7	5 1 6	nfbr	|- F/ x a R b
8		nfv	|- F/ x a = b
9	6 1 5	nfbr	|- F/ x b R a
10	7 8 9	nf3or	|- F/ x ( a R b \/ a = b \/ b R a )
11	2 10	nfralw	|- F/ x A. b e. A ( a R b \/ a = b \/ b R a )
12	2 11	nfralw	|- F/ x A. a e. A A. b e. A ( a R b \/ a = b \/ b R a )
13	4 12	nfan	|- F/ x ( R Po A /\ A. a e. A A. b e. A ( a R b \/ a = b \/ b R a ) )
14	3 13	nfxfr	|- F/ x R Or A