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

Metamath Proof Explorer

Theorem dfepfr

Description: An alternate way of saying that the membership relation is well-founded. (Contributed by NM, 17-Feb-2004) (Revised by Mario Carneiro, 23-Jun-2015)

Ref Expression
Assertion dfepfr ( E Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ 𝑦 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 dffr2 ⊢ ( E Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 E 𝑦 } = ∅ ) )
2 epel ⊢ ( 𝑧 E 𝑦 ↔ 𝑧 ∈ 𝑦 )
3 2 rabbii ⊢ { 𝑧 ∈ 𝑥 ∣ 𝑧 E 𝑦 } = { 𝑧 ∈ 𝑥 ∣ 𝑧 ∈ 𝑦 }
4 dfin5 ⊢ ( 𝑥 ∩ 𝑦 ) = { 𝑧 ∈ 𝑥 ∣ 𝑧 ∈ 𝑦 }
5 3 4 eqtr4i ⊢ { 𝑧 ∈ 𝑥 ∣ 𝑧 E 𝑦 } = ( 𝑥 ∩ 𝑦 )
6 5 eqeq1i ⊢ ( { 𝑧 ∈ 𝑥 ∣ 𝑧 E 𝑦 } = ∅ ↔ ( 𝑥 ∩ 𝑦 ) = ∅ )
7 6 rexbii ⊢ ( ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 E 𝑦 } = ∅ ↔ ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ 𝑦 ) = ∅ )
8 7 imbi2i ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 E 𝑦 } = ∅ ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ 𝑦 ) = ∅ ) )
9 8 albii ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 E 𝑦 } = ∅ ) ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ 𝑦 ) = ∅ ) )
10 1 9 bitri ⊢ ( E Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ 𝑦 ) = ∅ ) )