Metamath Proof Explorer

Theorem dffr7

Description: Alternate quantifier-free definition of a well-founded relation. (Contributed by Scott Fenton, 26-Aug-2026)

Ref Expression
Assertion dffr7 ⊢ R Fr A ↔ 𝒫 A ∖ ∅ ⊆ 𝖥𝗂𝗑 E ∘ V ∖ R ∘ E -1

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 1 elfix ⊢ x ∈ 𝖥𝗂𝗑 E ∘ V ∖ R ∘ E -1 ↔ x E ∘ V ∖ R ∘ E -1 x
3 1 1 coep ⊢ x E ∘ V ∖ R ∘ E -1 x ↔ ∃ y ∈ x x V ∖ R ∘ E -1 y
4 vex ⊢ y ∈ V
5 1 4 coepr ⊢ x R ∘ E -1 y ↔ ∃ z ∈ x z R y
6 5 notbii ⊢ ¬ x R ∘ E -1 y ↔ ¬ ∃ z ∈ x z R y
7 brv ⊢ x V y
8 brdif ⊢ x V ∖ R ∘ E -1 y ↔ x V y ∧ ¬ x R ∘ E -1 y
9 7 8 mpbiran ⊢ x V ∖ R ∘ E -1 y ↔ ¬ x R ∘ E -1 y
10 ralnex ⊢ ∀ z ∈ x ¬ z R y ↔ ¬ ∃ z ∈ x z R y
11 6 9 10 3bitr4i ⊢ x V ∖ R ∘ E -1 y ↔ ∀ z ∈ x ¬ z R y
12 11 rexbii ⊢ ∃ y ∈ x x V ∖ R ∘ E -1 y ↔ ∃ y ∈ x ∀ z ∈ x ¬ z R y
13 2 3 12 3bitri ⊢ x ∈ 𝖥𝗂𝗑 E ∘ V ∖ R ∘ E -1 ↔ ∃ y ∈ x ∀ z ∈ x ¬ z R y
14 13 ralbii ⊢ ∀ x ∈ 𝒫 A ∖ ∅ x ∈ 𝖥𝗂𝗑 E ∘ V ∖ R ∘ E -1 ↔ ∀ x ∈ 𝒫 A ∖ ∅ ∃ y ∈ x ∀ z ∈ x ¬ z R y
15 dfss3 ⊢ 𝒫 A ∖ ∅ ⊆ 𝖥𝗂𝗑 E ∘ V ∖ R ∘ E -1 ↔ ∀ x ∈ 𝒫 A ∖ ∅ x ∈ 𝖥𝗂𝗑 E ∘ V ∖ R ∘ E -1
16 dffr6 ⊢ R Fr A ↔ ∀ x ∈ 𝒫 A ∖ ∅ ∃ y ∈ x ∀ z ∈ x ¬ z R y
17 14 15 16 3bitr4ri ⊢ R Fr A ↔ 𝒫 A ∖ ∅ ⊆ 𝖥𝗂𝗑 E ∘ V ∖ R ∘ E -1