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 ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )

Proof

Step Hyp Ref Expression
1 velpw ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
2 1 bicomi ⊢ ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ∈ 𝒫 𝐴 )
3 velsn ⊢ ( 𝑥 ∈ { ∅ } ↔ 𝑥 = ∅ )
4 3 bicomi ⊢ ( 𝑥 = ∅ ↔ 𝑥 ∈ { ∅ } )
5 4 necon3abii ⊢ ( 𝑥 ≠ ∅ ↔ ¬ 𝑥 ∈ { ∅ } )
6 2 5 anbi12i ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ¬ 𝑥 ∈ { ∅ } ) )
7 eldif ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ¬ 𝑥 ∈ { ∅ } ) )
8 6 7 bitr4i ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ↔ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
9 8 imbi1i ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) ↔ ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
10 9 albii ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
11 df-fr ⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
12 df-ral ⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
13 10 11 12 3bitr4i ⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )