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 ⊢ Ⅎ _ x R
nffr.a ⊢ Ⅎ _ x A
Assertion nffr ⊢ Ⅎ x R Fr A

Proof

Step Hyp Ref Expression
1 nffr.r ⊢ Ⅎ _ x R
2 nffr.a ⊢ Ⅎ _ x A
3 df-fr ⊢ R Fr A ↔ ∀ a a ⊆ A ∧ a ≠ ∅ → ∃ b ∈ a ∀ c ∈ a ¬ c R b
4 nfcv ⊢ Ⅎ _ x a
5 4 2 nfss ⊢ Ⅎ x a ⊆ A
6 nfv ⊢ Ⅎ x a ≠ ∅
7 5 6 nfan ⊢ Ⅎ x a ⊆ A ∧ a ≠ ∅
8 nfcv ⊢ Ⅎ _ x c
9 nfcv ⊢ Ⅎ _ x b
10 8 1 9 nfbr ⊢ Ⅎ x c R b
11 10 nfn ⊢ Ⅎ x ¬ c R b
12 4 11 nfralw ⊢ Ⅎ x ∀ c ∈ a ¬ c R b
13 4 12 nfrexw ⊢ Ⅎ x ∃ b ∈ a ∀ c ∈ a ¬ c R b
14 7 13 nfim ⊢ Ⅎ x a ⊆ A ∧ a ≠ ∅ → ∃ b ∈ a ∀ c ∈ a ¬ c R b
15 14 nfal ⊢ Ⅎ x ∀ a a ⊆ A ∧ a ≠ ∅ → ∃ b ∈ a ∀ c ∈ a ¬ c R b
16 3 15 nfxfr ⊢ Ⅎ x R Fr A