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 ⊢RFrA↔𝒫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 ⊢yE∖E∘R-1x↔yEx∧¬yE∘R-1x
8 epel ⊢yEx↔y∈x
9 vex ⊢y∈V
10 vex ⊢x∈V
11 9 10 coep ⊢yE∘R-1x↔∃z∈xyR-1z
12 vex ⊢z∈V
13 9 12 brcnv ⊢yR-1z↔zRy
14 13 rexbii ⊢∃z∈xyR-1z↔∃z∈xzRy
15 dfrex2 ⊢∃z∈xzRy↔¬∀z∈x¬zRy
16 11 14 15 3bitrri ⊢¬∀z∈x¬zRy↔yE∘R-1x
17 16 con1bii ⊢¬yE∘R-1x↔∀z∈x¬zRy
18 8 17 anbi12i ⊢yEx∧¬yE∘R-1x↔y∈x∧∀z∈x¬zRy
19 7 18 bitri ⊢yE∖E∘R-1x↔y∈x∧∀z∈x¬zRy
20 19 exbii ⊢∃yyE∖E∘R-1x↔∃yy∈x∧∀z∈x¬zRy
21 10 elrn ⊢x∈ran⁡E∖E∘R-1↔∃yyE∖E∘R-1x
22 df-rex ⊢∃y∈x∀z∈x¬zRy↔∃yy∈x∧∀z∈x¬zRy
23 20 21 22 3bitr4i ⊢x∈ran⁡E∖E∘R-1↔∃y∈x∀z∈x¬zRy
24 6 23 imbi12i ⊢x∈𝒫A∖∅→x∈ran⁡E∖E∘R-1↔x⊆A∧x≠∅→∃y∈x∀z∈x¬zRy
25 24 albii ⊢∀xx∈𝒫A∖∅→x∈ran⁡E∖E∘R-1↔∀xx⊆A∧x≠∅→∃y∈x∀z∈x¬zRy
26 dfss2 ⊢𝒫A∖∅⊆ran⁡E∖E∘R-1↔∀xx∈𝒫A∖∅→x∈ran⁡E∖E∘R-1
27 df-fr ⊢RFrA↔∀xx⊆A∧x≠∅→∃y∈x∀z∈x¬zRy
28 25 26 27 3bitr4ri ⊢RFrA↔𝒫A∖∅⊆ran⁡E∖E∘R-1