Metamath Proof Explorer

Theorem dffr2

Description: Alternate definition of well-founded relation. Similar to Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 17-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by Mario Carneiro, 23-Jun-2015) Avoid ax-10 , ax-11 , ax-12 , but use ax-8 . (Revised by GG, 3-Oct-2024)

Ref Expression
Assertion dffr2 ⊢ R Fr A ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x z ∈ x | z R y = ∅

Proof

Step Hyp Ref Expression
1 df-fr ⊢ R Fr A ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ w ∈ x ¬ w R y
2 breq1 ⊢ z = w → z R y ↔ w R y
3 2 rabeq0w ⊢ z ∈ x | z R y = ∅ ↔ ∀ w ∈ x ¬ w R y
4 3 rexbii ⊢ ∃ y ∈ x z ∈ x | z R y = ∅ ↔ ∃ y ∈ x ∀ w ∈ x ¬ w R y
5 4 imbi2i ⊢ x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x z ∈ x | z R y = ∅ ↔ x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ w ∈ x ¬ w R y
6 5 albii ⊢ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x z ∈ x | z R y = ∅ ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ w ∈ x ¬ w R y
7 1 6 bitr4i ⊢ R Fr A ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x z ∈ x | z R y = ∅