Description: Bound-variable hypothesis builder for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018) (Proof shortened by AV, 10-Oct-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfwsuc.1 | ⊢ Ⅎ 𝑥 𝑅 | |
| nfwsuc.2 | ⊢ Ⅎ 𝑥 𝐴 | ||
| nfwsuc.3 | ⊢ Ⅎ 𝑥 𝑋 | ||
| Assertion | nfwsuc | ⊢ Ⅎ 𝑥 wsuc ( 𝑅 , 𝐴 , 𝑋 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfwsuc.1 | ⊢ Ⅎ 𝑥 𝑅 | |
| 2 | nfwsuc.2 | ⊢ Ⅎ 𝑥 𝐴 | |
| 3 | nfwsuc.3 | ⊢ Ⅎ 𝑥 𝑋 | |
| 4 | df-wsuc | ⊢ wsuc ( 𝑅 , 𝐴 , 𝑋 ) = inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) | |
| 5 | 1 | nfcnv | ⊢ Ⅎ 𝑥 ◡ 𝑅 |
| 6 | 5 2 3 | nfpred | ⊢ Ⅎ 𝑥 Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) |
| 7 | 6 2 1 | nfinf | ⊢ Ⅎ 𝑥 inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) |
| 8 | 4 7 | nfcxfr | ⊢ Ⅎ 𝑥 wsuc ( 𝑅 , 𝐴 , 𝑋 ) |