Theorem dffr2

Description: Alternate definition of well-founded relation. Similar to Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 17-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by Mario Carneiro, 23-Jun-2015) Avoid ax-10 , ax-11 , ax-12 , but use ax-8 . (Revised by GG, 3-Oct-2024)

	Ref	Expression
Assertion	dffr2	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		df-fr	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ¬ 𝑤 𝑅 𝑦 ) )
2		breq1	⊢ ( 𝑧 = 𝑤 → ( 𝑧 𝑅 𝑦 ↔ 𝑤 𝑅 𝑦 ) )
3	2	rabeq0w	⊢ ( { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ ↔ ∀ 𝑤 ∈ 𝑥 ¬ 𝑤 𝑅 𝑦 )
4	3	rexbii	⊢ ( ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ ↔ ∃ 𝑦 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ¬ 𝑤 𝑅 𝑦 )
5	4	imbi2i	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ¬ 𝑤 𝑅 𝑦 ) )
6	5	albii	⊢ ( ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ ) ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ¬ 𝑤 𝑅 𝑦 ) )
7	1 6	bitr4i	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ ) )