Metamath Proof Explorer

Theorem dffr5

Description: A quantifier-free definition of a well-founded relation. (Contributed by Scott Fenton, 11-Apr-2011) (Proof shortened by Scott Fenton, 26-Aug-2026)

Ref Expression
Assertion dffr5 ⊢ R Fr A ↔ 𝒫 A ∖ ∅ ⊆ ran ⁡ E ∖ E ∘ R -1

Proof

Step Hyp Ref Expression
1 brdif ⊢ y E ∖ E ∘ R -1 x ↔ y E x ∧ ¬ y E ∘ R -1 x
2 epel ⊢ y E x ↔ y ∈ x
3 vex ⊢ y ∈ V
4 vex ⊢ x ∈ V
5 3 4 coep ⊢ y E ∘ R -1 x ↔ ∃ z ∈ x y R -1 z
6 vex ⊢ z ∈ V
7 3 6 brcnv ⊢ y R -1 z ↔ z R y
8 7 rexbii ⊢ ∃ z ∈ x y R -1 z ↔ ∃ z ∈ x z R y
9 dfrex2 ⊢ ∃ z ∈ x z R y ↔ ¬ ∀ z ∈ x ¬ z R y
10 5 8 9 3bitrri ⊢ ¬ ∀ z ∈ x ¬ z R y ↔ y E ∘ R -1 x
11 10 con1bii ⊢ ¬ y E ∘ R -1 x ↔ ∀ z ∈ x ¬ z R y
12 2 11 anbi12i ⊢ y E x ∧ ¬ y E ∘ R -1 x ↔ y ∈ x ∧ ∀ z ∈ x ¬ z R y
13 1 12 bitri ⊢ y E ∖ E ∘ R -1 x ↔ y ∈ x ∧ ∀ z ∈ x ¬ z R y
14 13 exbii ⊢ ∃ y y E ∖ E ∘ R -1 x ↔ ∃ y y ∈ x ∧ ∀ z ∈ x ¬ z R y
15 4 elrn ⊢ x ∈ ran ⁡ E ∖ E ∘ R -1 ↔ ∃ y y E ∖ E ∘ R -1 x
16 df-rex ⊢ ∃ y ∈ x ∀ z ∈ x ¬ z R y ↔ ∃ y y ∈ x ∧ ∀ z ∈ x ¬ z R y
17 14 15 16 3bitr4i ⊢ x ∈ ran ⁡ E ∖ E ∘ R -1 ↔ ∃ y ∈ x ∀ z ∈ x ¬ z R y
18 17 ralbii ⊢ ∀ x ∈ 𝒫 A ∖ ∅ x ∈ ran ⁡ E ∖ E ∘ R -1 ↔ ∀ x ∈ 𝒫 A ∖ ∅ ∃ y ∈ x ∀ z ∈ x ¬ z R y
19 dfss3 ⊢ 𝒫 A ∖ ∅ ⊆ ran ⁡ E ∖ E ∘ R -1 ↔ ∀ x ∈ 𝒫 A ∖ ∅ x ∈ ran ⁡ E ∖ E ∘ R -1
20 dffr6 ⊢ R Fr A ↔ ∀ x ∈ 𝒫 A ∖ ∅ ∃ y ∈ x ∀ z ∈ x ¬ z R y
21 18 19 20 3bitr4ri ⊢ R Fr A ↔ 𝒫 A ∖ ∅ ⊆ ran ⁡ E ∖ E ∘ R -1