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

Proof

Step Hyp Ref Expression
1 nfpo.r ⊢ Ⅎ _ x R
2 nfpo.a ⊢ Ⅎ _ x A
3 df-po ⊢ R Po A ↔ ∀ a ∈ A ∀ b ∈ A ∀ c ∈ A ¬ a R a ∧ a R b ∧ b R c → a R c
4 nfcv ⊢ Ⅎ _ x a
5 4 1 4 nfbr ⊢ Ⅎ x a R a
6 5 nfn ⊢ Ⅎ x ¬ a R a
7 nfcv ⊢ Ⅎ _ x b
8 4 1 7 nfbr ⊢ Ⅎ x a R b
9 nfcv ⊢ Ⅎ _ x c
10 7 1 9 nfbr ⊢ Ⅎ x b R c
11 8 10 nfan ⊢ Ⅎ x a R b ∧ b R c
12 4 1 9 nfbr ⊢ Ⅎ x a R c
13 11 12 nfim ⊢ Ⅎ x a R b ∧ b R c → a R c
14 6 13 nfan ⊢ Ⅎ x ¬ a R a ∧ a R b ∧ b R c → a R c
15 2 14 nfralw ⊢ Ⅎ x ∀ c ∈ A ¬ a R a ∧ a R b ∧ b R c → a R c
16 2 15 nfralw ⊢ Ⅎ x ∀ b ∈ A ∀ c ∈ A ¬ a R a ∧ a R b ∧ b R c → a R c
17 2 16 nfralw ⊢ Ⅎ x ∀ a ∈ A ∀ b ∈ A ∀ c ∈ A ¬ a R a ∧ a R b ∧ b R c → a R c
18 3 17 nfxfr ⊢ Ⅎ x R Po A