Theorem dffr4

Description: Alternate definition of well-founded relation. (Contributed by Scott Fenton, 2-Feb-2011)

	Ref	Expression
Assertion	dffr4	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝑥 , 𝑦 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		dffr3	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
2		df-pred	⊢ Pred ( 𝑅 , 𝑥 , 𝑦 ) = ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) )
3	2	eqeq1i	⊢ ( Pred ( 𝑅 , 𝑥 , 𝑦 ) = ∅ ↔ ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ )
4	3	rexbii	⊢ ( ∃ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝑥 , 𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ )
5	4	imbi2i	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝑥 , 𝑦 ) = ∅ ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
6	5	albii	⊢ ( ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝑥 , 𝑦 ) = ∅ ) ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
7	1 6	bitr4i	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝑥 , 𝑦 ) = ∅ ) )