ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfpo GIF version

Theorem nfpo 4302
Description: Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
Hypotheses
Ref Expression
nfpo.r 𝑥𝑅
nfpo.a 𝑥𝐴
Assertion
Ref Expression
nfpo 𝑥 𝑅 Po 𝐴

Proof of Theorem nfpo
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-po 4297 . 2 (𝑅 Po 𝐴 ↔ ∀𝑎𝐴𝑏𝐴𝑐𝐴𝑎𝑅𝑎 ∧ ((𝑎𝑅𝑏𝑏𝑅𝑐) → 𝑎𝑅𝑐)))
2 nfpo.a . . 3 𝑥𝐴
3 nfcv 2319 . . . . . . . 8 𝑥𝑎
4 nfpo.r . . . . . . . 8 𝑥𝑅
53, 4, 3nfbr 4050 . . . . . . 7 𝑥 𝑎𝑅𝑎
65nfn 1658 . . . . . 6 𝑥 ¬ 𝑎𝑅𝑎
7 nfcv 2319 . . . . . . . . 9 𝑥𝑏
83, 4, 7nfbr 4050 . . . . . . . 8 𝑥 𝑎𝑅𝑏
9 nfcv 2319 . . . . . . . . 9 𝑥𝑐
107, 4, 9nfbr 4050 . . . . . . . 8 𝑥 𝑏𝑅𝑐
118, 10nfan 1565 . . . . . . 7 𝑥(𝑎𝑅𝑏𝑏𝑅𝑐)
123, 4, 9nfbr 4050 . . . . . . 7 𝑥 𝑎𝑅𝑐
1311, 12nfim 1572 . . . . . 6 𝑥((𝑎𝑅𝑏𝑏𝑅𝑐) → 𝑎𝑅𝑐)
146, 13nfan 1565 . . . . 5 𝑥𝑎𝑅𝑎 ∧ ((𝑎𝑅𝑏𝑏𝑅𝑐) → 𝑎𝑅𝑐))
152, 14nfralxy 2515 . . . 4 𝑥𝑐𝐴𝑎𝑅𝑎 ∧ ((𝑎𝑅𝑏𝑏𝑅𝑐) → 𝑎𝑅𝑐))
162, 15nfralxy 2515 . . 3 𝑥𝑏𝐴𝑐𝐴𝑎𝑅𝑎 ∧ ((𝑎𝑅𝑏𝑏𝑅𝑐) → 𝑎𝑅𝑐))
172, 16nfralxy 2515 . 2 𝑥𝑎𝐴𝑏𝐴𝑐𝐴𝑎𝑅𝑎 ∧ ((𝑎𝑅𝑏𝑏𝑅𝑐) → 𝑎𝑅𝑐))
181, 17nfxfr 1474 1 𝑥 𝑅 Po 𝐴
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wnf 1460  wnfc 2306  wral 2455   class class class wbr 4004   Po wpo 4295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005  df-po 4297
This theorem is referenced by:  nfso  4303
  Copyright terms: Public domain W3C validator