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

Metamath Proof Explorer

Theorem dffr6

Description: Alternate definition of df-fr . See dffr5 for a definition without dummy variables (but note that their equivalence uses ax-sep ). (Contributed by BJ, 16-Nov-2024)

Ref Expression
Assertion dffr6 ⊢ R Fr A ↔ ∀ x ∈ 𝒫 A ∖ ∅ ∃ y ∈ x ∀ z ∈ x ¬ z R y

Proof

Step Hyp Ref Expression
1 velpw ⊢ x ∈ 𝒫 A ↔ x ⊆ A
2 1 bicomi ⊢ x ⊆ A ↔ x ∈ 𝒫 A
3 velsn ⊢ x ∈ ∅ ↔ x = ∅
4 3 bicomi ⊢ x = ∅ ↔ x ∈ ∅
5 4 necon3abii ⊢ x ≠ ∅ ↔ ¬ x ∈ ∅
6 2 5 anbi12i ⊢ x ⊆ A ∧ x ≠ ∅ ↔ x ∈ 𝒫 A ∧ ¬ x ∈ ∅
7 eldif ⊢ x ∈ 𝒫 A ∖ ∅ ↔ x ∈ 𝒫 A ∧ ¬ x ∈ ∅
8 6 7 bitr4i ⊢ x ⊆ A ∧ x ≠ ∅ ↔ x ∈ 𝒫 A ∖ ∅
9 8 imbi1i ⊢ x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y ↔ x ∈ 𝒫 A ∖ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y
10 9 albii ⊢ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y ↔ ∀ x x ∈ 𝒫 A ∖ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y
11 df-fr ⊢ R Fr A ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y
12 df-ral ⊢ ∀ x ∈ 𝒫 A ∖ ∅ ∃ y ∈ x ∀ z ∈ x ¬ z R y ↔ ∀ x x ∈ 𝒫 A ∖ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y
13 10 11 12 3bitr4i ⊢ R Fr A ↔ ∀ x ∈ 𝒫 A ∖ ∅ ∃ y ∈ x ∀ z ∈ x ¬ z R y