Theorem fr0

Description: Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993)

	Ref	Expression
Assertion	fr0	⊢ 𝑅 Fr ∅

Proof

Step	Hyp	Ref	Expression
1		dffr2	⊢ ( 𝑅 Fr ∅ ↔ ∀ 𝑥 ( ( 𝑥 ⊆ ∅ ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ ) )
2		ss0	⊢ ( 𝑥 ⊆ ∅ → 𝑥 = ∅ )
3	2	a1d	⊢ ( 𝑥 ⊆ ∅ → ( ¬ ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ → 𝑥 = ∅ ) )
4	3	necon1ad	⊢ ( 𝑥 ⊆ ∅ → ( 𝑥 ≠ ∅ → ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ ) )
5	4	imp	⊢ ( ( 𝑥 ⊆ ∅ ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑧 𝑅 𝑦 } = ∅ )
6	1 5	mpgbir	⊢ 𝑅 Fr ∅