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

Metamath Proof Explorer

Theorem dffr5

Description: A quantifier-free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011)

Ref Expression
Assertion dffr5 ( 𝑅 Fr 𝐴 ↔ ( 𝒫 𝐴 ∖ { ∅ } ) ⊆ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 eldif ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ¬ 𝑥 ∈ { ∅ } ) )
2 velpw ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
3 velsn ⊢ ( 𝑥 ∈ { ∅ } ↔ 𝑥 = ∅ )
4 3 necon3bbii ⊢ ( ¬ 𝑥 ∈ { ∅ } ↔ 𝑥 ≠ ∅ )
5 2 4 anbi12i ⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ¬ 𝑥 ∈ { ∅ } ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) )
6 1 5 bitri ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) )
7 brdif ⊢ ( 𝑦 ( E ∖ ( E ∘ ◡ 𝑅 ) ) 𝑥 ↔ ( 𝑦 E 𝑥 ∧ ¬ 𝑦 ( E ∘ ◡ 𝑅 ) 𝑥 ) )
8 epel ⊢ ( 𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥 )
9 vex ⊢ 𝑦 ∈ V
10 vex ⊢ 𝑥 ∈ V
11 9 10 coep ⊢ ( 𝑦 ( E ∘ ◡ 𝑅 ) 𝑥 ↔ ∃ 𝑧 ∈ 𝑥 𝑦 ◡ 𝑅 𝑧 )
12 vex ⊢ 𝑧 ∈ V
13 9 12 brcnv ⊢ ( 𝑦 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑦 )
14 13 rexbii ⊢ ( ∃ 𝑧 ∈ 𝑥 𝑦 ◡ 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝑥 𝑧 𝑅 𝑦 )
15 dfrex2 ⊢ ( ∃ 𝑧 ∈ 𝑥 𝑧 𝑅 𝑦 ↔ ¬ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
16 11 14 15 3bitrri ⊢ ( ¬ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ↔ 𝑦 ( E ∘ ◡ 𝑅 ) 𝑥 )
17 16 con1bii ⊢ ( ¬ 𝑦 ( E ∘ ◡ 𝑅 ) 𝑥 ↔ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
18 8 17 anbi12i ⊢ ( ( 𝑦 E 𝑥 ∧ ¬ 𝑦 ( E ∘ ◡ 𝑅 ) 𝑥 ) ↔ ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
19 7 18 bitri ⊢ ( 𝑦 ( E ∖ ( E ∘ ◡ 𝑅 ) ) 𝑥 ↔ ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
20 19 exbii ⊢ ( ∃ 𝑦 𝑦 ( E ∖ ( E ∘ ◡ 𝑅 ) ) 𝑥 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
21 10 elrn ⊢ ( 𝑥 ∈ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) ↔ ∃ 𝑦 𝑦 ( E ∖ ( E ∘ ◡ 𝑅 ) ) 𝑥 )
22 df-rex ⊢ ( ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
23 20 21 22 3bitr4i ⊢ ( 𝑥 ∈ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) ↔ ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
24 6 23 imbi12i ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → 𝑥 ∈ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
25 24 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → 𝑥 ∈ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) ) ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
26 df-ss ⊢ ( ( 𝒫 𝐴 ∖ { ∅ } ) ⊆ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → 𝑥 ∈ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) ) )
27 df-fr ⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
28 25 26 27 3bitr4ri ⊢ ( 𝑅 Fr 𝐴 ↔ ( 𝒫 𝐴 ∖ { ∅ } ) ⊆ ran ( E ∖ ( E ∘ ◡ 𝑅 ) ) )