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

Metamath Proof Explorer

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 ( 𝑅 , 𝑥 , 𝑦 ) = ∅ ) )