This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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