Metamath Proof Explorer

Theorem fri

Description: Property of well-founded relation (one direction of definition). (Contributed by NM, 18-Mar-1997)

Ref Expression
Assertion fri ⊢ B ∈ C ∧ R Fr A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x

Proof

Step Hyp Ref Expression
1 df-fr ⊢ R Fr A ↔ ∀ z z ⊆ A ∧ z ≠ ∅ → ∃ x ∈ z ∀ y ∈ z ¬ y R x
2 sseq1 ⊢ z = B → z ⊆ A ↔ B ⊆ A
3 neeq1 ⊢ z = B → z ≠ ∅ ↔ B ≠ ∅
4 2 3 anbi12d ⊢ z = B → z ⊆ A ∧ z ≠ ∅ ↔ B ⊆ A ∧ B ≠ ∅
5 raleq ⊢ z = B → ∀ y ∈ z ¬ y R x ↔ ∀ y ∈ B ¬ y R x
6 5 rexeqbi1dv ⊢ z = B → ∃ x ∈ z ∀ y ∈ z ¬ y R x ↔ ∃ x ∈ B ∀ y ∈ B ¬ y R x
7 4 6 imbi12d ⊢ z = B → z ⊆ A ∧ z ≠ ∅ → ∃ x ∈ z ∀ y ∈ z ¬ y R x ↔ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
8 7 spcgv ⊢ B ∈ C → ∀ z z ⊆ A ∧ z ≠ ∅ → ∃ x ∈ z ∀ y ∈ z ¬ y R x → B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
9 1 8 syl5bi ⊢ B ∈ C → R Fr A → B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
10 9 imp31 ⊢ B ∈ C ∧ R Fr A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x