This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴