Theorem dffr3

Description: Alternate definition of well-founded relation. Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 23-Apr-2004) (Revised by Mario Carneiro, 23-Jun-2015)

	Ref	Expression
Assertion	dffr3	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		dffr2	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ ) )
2		iniseg	⊢ ( 𝑦 ∈ V → ( ◡ 𝑅 “ { 𝑦 } ) = { 𝑧 ∣ 𝑧 𝑅 𝑦 } )
3	2	elv	⊢ ( ◡ 𝑅 “ { 𝑦 } ) = { 𝑧 ∣ 𝑧 𝑅 𝑦 }
4	3	ineq2i	⊢ ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ( 𝑥 ∩ { 𝑧 ∣ 𝑧 𝑅 𝑦 } )
5		dfrab3	⊢ { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ( 𝑥 ∩ { 𝑧 ∣ 𝑧 𝑅 𝑦 } )
6	4 5	eqtr4i	⊢ ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 }
7	6	eqeq1i	⊢ ( ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ↔ { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ )
8	7	rexbii	⊢ ( ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ↔ ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ )
9	8	imbi2i	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ ) )
10	9	albii	⊢ ( ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ ) )
11	1 10	bitr4i	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )