Theorem frd

Description: A nonempty subset of an R -well-founded class has an R -minimal element (deduction form). (Contributed by BJ, 16-Nov-2024)

	Ref	Expression
Hypotheses	frd.fr	⊢ ( 𝜑 → 𝑅 Fr 𝐴 )
	frd.ss	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
	frd.ex	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	frd.n0	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
Assertion	frd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		frd.fr	⊢ ( 𝜑 → 𝑅 Fr 𝐴 )
2		frd.ss	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
3		frd.ex	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4		frd.n0	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
5		simpr	⊢ ( ( 𝜑 ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐵 )
6		biidd	⊢ ( ( 𝜑 ∧ 𝑧 = 𝐵 ) → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝑥 ) )
7	5 6	raleqbidv	⊢ ( ( 𝜑 ∧ 𝑧 = 𝐵 ) → ( ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
8	5 7	rexeqbidv	⊢ ( ( 𝜑 ∧ 𝑧 = 𝐵 ) → ( ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
9	3 2	elpwd	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝐴 )
10		nelsn	⊢ ( 𝐵 ≠ ∅ → ¬ 𝐵 ∈ { ∅ } )
11	4 10	syl	⊢ ( 𝜑 → ¬ 𝐵 ∈ { ∅ } )
12	9 11	eldifd	⊢ ( 𝜑 → 𝐵 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
13		dffr6	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑧 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 )
14	1 13	sylib	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 )
15	8 12 14	rspcdv2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )