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

Metamath Proof Explorer

Theorem nfpo

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

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

Proof

Step Hyp Ref Expression
1 nfpo.r ⊢ Ⅎ 𝑥 𝑅
2 nfpo.a ⊢ Ⅎ 𝑥 𝐴
3 df-po ⊢ ( 𝑅 Po 𝐴 ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ 𝐴 ( ¬ 𝑎 𝑅 𝑎 ∧ ( ( 𝑎 𝑅 𝑏 ∧ 𝑏 𝑅 𝑐 ) → 𝑎 𝑅 𝑐 ) ) )
4 nfcv ⊢ Ⅎ 𝑥 𝑎
5 4 1 4 nfbr ⊢ Ⅎ 𝑥 𝑎 𝑅 𝑎
6 5 nfn ⊢ Ⅎ 𝑥 ¬ 𝑎 𝑅 𝑎
7 nfcv ⊢ Ⅎ 𝑥 𝑏
8 4 1 7 nfbr ⊢ Ⅎ 𝑥 𝑎 𝑅 𝑏
9 nfcv ⊢ Ⅎ 𝑥 𝑐
10 7 1 9 nfbr ⊢ Ⅎ 𝑥 𝑏 𝑅 𝑐
11 8 10 nfan ⊢ Ⅎ 𝑥 ( 𝑎 𝑅 𝑏 ∧ 𝑏 𝑅 𝑐 )
12 4 1 9 nfbr ⊢ Ⅎ 𝑥 𝑎 𝑅 𝑐
13 11 12 nfim ⊢ Ⅎ 𝑥 ( ( 𝑎 𝑅 𝑏 ∧ 𝑏 𝑅 𝑐 ) → 𝑎 𝑅 𝑐 )
14 6 13 nfan ⊢ Ⅎ 𝑥 ( ¬ 𝑎 𝑅 𝑎 ∧ ( ( 𝑎 𝑅 𝑏 ∧ 𝑏 𝑅 𝑐 ) → 𝑎 𝑅 𝑐 ) )
15 2 14 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑐 ∈ 𝐴 ( ¬ 𝑎 𝑅 𝑎 ∧ ( ( 𝑎 𝑅 𝑏 ∧ 𝑏 𝑅 𝑐 ) → 𝑎 𝑅 𝑐 ) )
16 2 15 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ 𝐴 ( ¬ 𝑎 𝑅 𝑎 ∧ ( ( 𝑎 𝑅 𝑏 ∧ 𝑏 𝑅 𝑐 ) → 𝑎 𝑅 𝑐 ) )
17 2 16 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ 𝐴 ( ¬ 𝑎 𝑅 𝑎 ∧ ( ( 𝑎 𝑅 𝑏 ∧ 𝑏 𝑅 𝑐 ) → 𝑎 𝑅 𝑐 ) )
18 3 17 nfxfr ⊢ Ⅎ 𝑥 𝑅 Po 𝐴