Theorem dffr7

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

	Ref	Expression
Assertion	dffr7	⊢ ( 𝑅 Fr 𝐴 ↔ ( 𝒫 𝐴 ∖ { ∅ } ) ⊆ Fix ( E ∘ ( V ∖ ( 𝑅 ∘ ◡ E ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	elfix	⊢ ( 𝑥 ∈ Fix ( E ∘ ( V ∖ ( 𝑅 ∘ ◡ E ) ) ) ↔ 𝑥 ( E ∘ ( V ∖ ( 𝑅 ∘ ◡ E ) ) ) 𝑥 )
3	1 1	coep	⊢ ( 𝑥 ( E ∘ ( V ∖ ( 𝑅 ∘ ◡ E ) ) ) 𝑥 ↔ ∃ 𝑦 ∈ 𝑥 𝑥 ( V ∖ ( 𝑅 ∘ ◡ E ) ) 𝑦 )
4		vex	⊢ 𝑦 ∈ V
5	1 4	coepr	⊢ ( 𝑥 ( 𝑅 ∘ ◡ E ) 𝑦 ↔ ∃ 𝑧 ∈ 𝑥 𝑧 𝑅 𝑦 )
6	5	notbii	⊢ ( ¬ 𝑥 ( 𝑅 ∘ ◡ E ) 𝑦 ↔ ¬ ∃ 𝑧 ∈ 𝑥 𝑧 𝑅 𝑦 )
7		brv	⊢ 𝑥 V 𝑦
8		brdif	⊢ ( 𝑥 ( V ∖ ( 𝑅 ∘ ◡ E ) ) 𝑦 ↔ ( 𝑥 V 𝑦 ∧ ¬ 𝑥 ( 𝑅 ∘ ◡ E ) 𝑦 ) )
9	7 8	mpbiran	⊢ ( 𝑥 ( V ∖ ( 𝑅 ∘ ◡ E ) ) 𝑦 ↔ ¬ 𝑥 ( 𝑅 ∘ ◡ E ) 𝑦 )
10		ralnex	⊢ ( ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ↔ ¬ ∃ 𝑧 ∈ 𝑥 𝑧 𝑅 𝑦 )
11	6 9 10	3bitr4i	⊢ ( 𝑥 ( V ∖ ( 𝑅 ∘ ◡ E ) ) 𝑦 ↔ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
12	11	rexbii	⊢ ( ∃ 𝑦 ∈ 𝑥 𝑥 ( V ∖ ( 𝑅 ∘ ◡ E ) ) 𝑦 ↔ ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
13	2 3 12	3bitri	⊢ ( 𝑥 ∈ Fix ( E ∘ ( V ∖ ( 𝑅 ∘ ◡ E ) ) ) ↔ ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
14	13	ralbii	⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) 𝑥 ∈ Fix ( E ∘ ( V ∖ ( 𝑅 ∘ ◡ E ) ) ) ↔ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
15		dfss3	⊢ ( ( 𝒫 𝐴 ∖ { ∅ } ) ⊆ Fix ( E ∘ ( V ∖ ( 𝑅 ∘ ◡ E ) ) ) ↔ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) 𝑥 ∈ Fix ( E ∘ ( V ∖ ( 𝑅 ∘ ◡ E ) ) ) )
16		dffr6	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
17	14 15 16	3bitr4ri	⊢ ( 𝑅 Fr 𝐴 ↔ ( 𝒫 𝐴 ∖ { ∅ } ) ⊆ Fix ( E ∘ ( V ∖ ( 𝑅 ∘ ◡ E ) ) ) )