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	⊢ ( 𝑅 Fr 𝐴 ↔ ( 𝒫 𝐴 ∖ { ∅ } ) ⊆ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		brdif	⊢ ( 𝑦 ( E ∖ ( E ∘ ◡ 𝑅 ) ) 𝑥 ↔ ( 𝑦 E 𝑥 ∧ ¬ 𝑦 ( E ∘ ◡ 𝑅 ) 𝑥 ) )
2		epel	⊢ ( 𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥 )
3		vex	⊢ 𝑦 ∈ V
4		vex	⊢ 𝑥 ∈ V
5	3 4	coep	⊢ ( 𝑦 ( E ∘ ◡ 𝑅 ) 𝑥 ↔ ∃ 𝑧 ∈ 𝑥 𝑦 ◡ 𝑅 𝑧 )
6		vex	⊢ 𝑧 ∈ V
7	3 6	brcnv	⊢ ( 𝑦 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑦 )
8	7	rexbii	⊢ ( ∃ 𝑧 ∈ 𝑥 𝑦 ◡ 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝑥 𝑧 𝑅 𝑦 )
9		dfrex2	⊢ ( ∃ 𝑧 ∈ 𝑥 𝑧 𝑅 𝑦 ↔ ¬ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
10	5 8 9	3bitrri	⊢ ( ¬ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ↔ 𝑦 ( E ∘ ◡ 𝑅 ) 𝑥 )
11	10	con1bii	⊢ ( ¬ 𝑦 ( E ∘ ◡ 𝑅 ) 𝑥 ↔ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
12	2 11	anbi12i	⊢ ( ( 𝑦 E 𝑥 ∧ ¬ 𝑦 ( E ∘ ◡ 𝑅 ) 𝑥 ) ↔ ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
13	1 12	bitri	⊢ ( 𝑦 ( E ∖ ( E ∘ ◡ 𝑅 ) ) 𝑥 ↔ ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
14	13	exbii	⊢ ( ∃ 𝑦 𝑦 ( E ∖ ( E ∘ ◡ 𝑅 ) ) 𝑥 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
15	4	elrn	⊢ ( 𝑥 ∈ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) ↔ ∃ 𝑦 𝑦 ( E ∖ ( E ∘ ◡ 𝑅 ) ) 𝑥 )
16		df-rex	⊢ ( ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
17	14 15 16	3bitr4i	⊢ ( 𝑥 ∈ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) ↔ ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
18	17	ralbii	⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) 𝑥 ∈ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) ↔ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
19		dfss3	⊢ ( ( 𝒫 𝐴 ∖ { ∅ } ) ⊆ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) ↔ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) 𝑥 ∈ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) )
20		dffr6	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
21	18 19 20	3bitr4ri	⊢ ( 𝑅 Fr 𝐴 ↔ ( 𝒫 𝐴 ∖ { ∅ } ) ⊆ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) )