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

Proof

Step Hyp Ref Expression
1 nfpo.r 
 |-  F/_ x R
2 nfpo.a 
 |-  F/_ x A
3 df-po 
 |-  ( R Po A <-> A. a e. A A. b e. A A. c e. A ( -. a R a /\ ( ( a R b /\ b R c ) -> a R c ) ) )
4 nfcv 
 |-  F/_ x a
5 4 1 4 nfbr 
 |-  F/ x a R a
6 5 nfn 
 |-  F/ x -. a R a
7 nfcv 
 |-  F/_ x b
8 4 1 7 nfbr 
 |-  F/ x a R b
9 nfcv 
 |-  F/_ x c
10 7 1 9 nfbr 
 |-  F/ x b R c
11 8 10 nfan 
 |-  F/ x ( a R b /\ b R c )
12 4 1 9 nfbr 
 |-  F/ x a R c
13 11 12 nfim 
 |-  F/ x ( ( a R b /\ b R c ) -> a R c )
14 6 13 nfan 
 |-  F/ x ( -. a R a /\ ( ( a R b /\ b R c ) -> a R c ) )
15 2 14 nfralw 
 |-  F/ x A. c e. A ( -. a R a /\ ( ( a R b /\ b R c ) -> a R c ) )
16 2 15 nfralw 
 |-  F/ x A. b e. A A. c e. A ( -. a R a /\ ( ( a R b /\ b R c ) -> a R c ) )
17 2 16 nfralw 
 |-  F/ x A. a e. A A. b e. A A. c e. A ( -. a R a /\ ( ( a R b /\ b R c ) -> a R c ) )
18 3 17 nfxfr 
 |-  F/ x R Po A