This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nffr

Description: Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015) (Revised by Mario Carneiro, 14-Oct-2016)

Ref Expression
Hypotheses nffr.r ⊢ Ⅎ 𝑥 𝑅
nffr.a ⊢ Ⅎ 𝑥 𝐴
Assertion nffr Ⅎ 𝑥 𝑅 Fr 𝐴

Proof

Step Hyp Ref Expression
1 nffr.r ⊢ Ⅎ 𝑥 𝑅
2 nffr.a ⊢ Ⅎ 𝑥 𝐴
3 df-fr ⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑎 ( ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑅 𝑏 ) )
4 nfcv ⊢ Ⅎ 𝑥 𝑎
5 4 2 nfss ⊢ Ⅎ 𝑥 𝑎 ⊆ 𝐴
6 nfv ⊢ Ⅎ 𝑥 𝑎 ≠ ∅
7 5 6 nfan ⊢ Ⅎ 𝑥 ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ )
8 nfcv ⊢ Ⅎ 𝑥 𝑐
9 nfcv ⊢ Ⅎ 𝑥 𝑏
10 8 1 9 nfbr ⊢ Ⅎ 𝑥 𝑐 𝑅 𝑏
11 10 nfn ⊢ Ⅎ 𝑥 ¬ 𝑐 𝑅 𝑏
12 4 11 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑅 𝑏
13 4 12 nfrexw ⊢ Ⅎ 𝑥 ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑅 𝑏
14 7 13 nfim ⊢ Ⅎ 𝑥 ( ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑅 𝑏 )
15 14 nfal ⊢ Ⅎ 𝑥 ∀ 𝑎 ( ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑅 𝑏 )
16 3 15 nfxfr ⊢ Ⅎ 𝑥 𝑅 Fr 𝐴