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 𝐴