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 ⊢ Ⅎ _ x R
nfpo.a ⊢ Ⅎ _ x A
Assertion nfso ⊢ Ⅎ x R Or A

Proof

Step Hyp Ref Expression
1 nfpo.r ⊢ Ⅎ _ x R
2 nfpo.a ⊢ Ⅎ _ x A
3 df-so ⊢ R Or A ↔ R Po A ∧ ∀ a ∈ A ∀ b ∈ A a R b ∨ a = b ∨ b R a
4 1 2 nfpo ⊢ Ⅎ x R Po A
5 nfcv ⊢ Ⅎ _ x a
6 nfcv ⊢ Ⅎ _ x b
7 5 1 6 nfbr ⊢ Ⅎ x a R b
8 nfv ⊢ Ⅎ x a = b
9 6 1 5 nfbr ⊢ Ⅎ x b R a
10 7 8 9 nf3or ⊢ Ⅎ x a R b ∨ a = b ∨ b R a
11 2 10 nfralw ⊢ Ⅎ x ∀ b ∈ A a R b ∨ a = b ∨ b R a
12 2 11 nfralw ⊢ Ⅎ x ∀ a ∈ A ∀ b ∈ A a R b ∨ a = b ∨ b R a
13 4 12 nfan ⊢ Ⅎ x R Po A ∧ ∀ a ∈ A ∀ b ∈ A a R b ∨ a = b ∨ b R a
14 3 13 nfxfr ⊢ Ⅎ x R Or A