Metamath Proof Explorer

Theorem dffr5

Description: A quantifier-free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011)

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

Proof

Step Hyp Ref Expression
1 eldif ⊢ x ∈ 𝒫 A ∖ ∅ ↔ x ∈ 𝒫 A ∧ ¬ x ∈ ∅
2 velpw ⊢ x ∈ 𝒫 A ↔ x ⊆ A
3 velsn ⊢ x ∈ ∅ ↔ x = ∅
4 3 necon3bbii ⊢ ¬ x ∈ ∅ ↔ x ≠ ∅
5 2 4 anbi12i ⊢ x ∈ 𝒫 A ∧ ¬ x ∈ ∅ ↔ x ⊆ A ∧ x ≠ ∅
6 1 5 bitri ⊢ x ∈ 𝒫 A ∖ ∅ ↔ x ⊆ A ∧ x ≠ ∅
7 brdif ⊢ y E ∖ E ∘ R -1 x ↔ y E x ∧ ¬ y E ∘ R -1 x
8 epel ⊢ y E x ↔ y ∈ x
9 vex ⊢ y ∈ V
10 vex ⊢ x ∈ V
11 9 10 coep ⊢ y E ∘ R -1 x ↔ ∃ z ∈ x y R -1 z
12 vex ⊢ z ∈ V
13 9 12 brcnv ⊢ y R -1 z ↔ z R y
14 13 rexbii ⊢ ∃ z ∈ x y R -1 z ↔ ∃ z ∈ x z R y
15 dfrex2 ⊢ ∃ z ∈ x z R y ↔ ¬ ∀ z ∈ x ¬ z R y
16 11 14 15 3bitrri ⊢ ¬ ∀ z ∈ x ¬ z R y ↔ y E ∘ R -1 x
17 16 con1bii ⊢ ¬ y E ∘ R -1 x ↔ ∀ z ∈ x ¬ z R y
18 8 17 anbi12i ⊢ y E x ∧ ¬ y E ∘ R -1 x ↔ y ∈ x ∧ ∀ z ∈ x ¬ z R y
19 7 18 bitri ⊢ y E ∖ E ∘ R -1 x ↔ y ∈ x ∧ ∀ z ∈ x ¬ z R y
20 19 exbii ⊢ ∃ y y E ∖ E ∘ R -1 x ↔ ∃ y y ∈ x ∧ ∀ z ∈ x ¬ z R y
21 10 elrn ⊢ x ∈ ran ⁡ E ∖ E ∘ R -1 ↔ ∃ y y E ∖ E ∘ R -1 x
22 df-rex ⊢ ∃ y ∈ x ∀ z ∈ x ¬ z R y ↔ ∃ y y ∈ x ∧ ∀ z ∈ x ¬ z R y
23 20 21 22 3bitr4i ⊢ x ∈ ran ⁡ E ∖ E ∘ R -1 ↔ ∃ y ∈ x ∀ z ∈ x ¬ z R y
24 6 23 imbi12i ⊢ x ∈ 𝒫 A ∖ ∅ → x ∈ ran ⁡ E ∖ E ∘ R -1 ↔ x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y
25 24 albii ⊢ ∀ x x ∈ 𝒫 A ∖ ∅ → x ∈ ran ⁡ E ∖ E ∘ R -1 ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y
26 dfss2 ⊢ 𝒫 A ∖ ∅ ⊆ ran ⁡ E ∖ E ∘ R -1 ↔ ∀ x x ∈ 𝒫 A ∖ ∅ → x ∈ ran ⁡ E ∖ E ∘ R -1
27 df-fr ⊢ R Fr A ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y
28 25 26 27 3bitr4ri ⊢ R Fr A ↔ 𝒫 A ∖ ∅ ⊆ ran ⁡ E ∖ E ∘ R -1