Theorem frpomin2

Description: Every nonempty (possibly proper) subclass of a class A with a well-founded set-like partial order R has a minimal element. The additional condition of partial order over frmin enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022)

	Ref	Expression
Assertion	frpomin2	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		frpomin	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
2		vex	⊢ 𝑥 ∈ V
3	2	dfpred3	⊢ Pred ( 𝑅 , 𝐵 , 𝑥 ) = { 𝑦 ∈ 𝐵 ∣ 𝑦 𝑅 𝑥 }
4	3	eqeq1i	⊢ ( Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ ↔ { 𝑦 ∈ 𝐵 ∣ 𝑦 𝑅 𝑥 } = ∅ )
5		rabeq0	⊢ ( { 𝑦 ∈ 𝐵 ∣ 𝑦 𝑅 𝑥 } = ∅ ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
6	4 5	bitri	⊢ ( Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
7	6	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
8	1 7	sylibr	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ )