Theorem dffr5

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

	Ref	Expression
Assertion	dffr5	⊢ ( 𝑅 Fr 𝐴 ↔ ( 𝒫 𝐴 ∖ { ∅ } ) ⊆ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) )

Proof

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