# Metamath Proof Explorer

## 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 𝐴 ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥 ( 𝑥 ∩ ( 𝑅 “ { 𝑦 } ) ) = ∅ ) )