Theorem frminex

Description: If an element of a well-founded set satisfies a property ph , then there is a minimal element that satisfies ph . (Contributed by Jeff Madsen, 18-Jun-2010) (Proof shortened by Mario Carneiro, 18-Nov-2016)

	Ref	Expression
Hypotheses	frminex.1	⊢ 𝐴 ∈ V
	frminex.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	frminex	⊢ ( 𝑅 Fr 𝐴 → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		frminex.1	⊢ 𝐴 ∈ V
2		frminex.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3		rabn0	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
4	1	rabex	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∈ V
5		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴
6		fri	⊢ ( ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ) ) → ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ¬ 𝑦 𝑅 𝑧 )
7	2	ralrab	⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ¬ 𝑦 𝑅 𝑧 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑧 ) )
8	7	rexbii	⊢ ( ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ¬ 𝑦 𝑅 𝑧 ↔ ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑧 ) )
9		breq2	⊢ ( 𝑧 = 𝑥 → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑅 𝑥 ) )
10	9	notbid	⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑦 𝑅 𝑧 ↔ ¬ 𝑦 𝑅 𝑥 ) )
11	10	imbi2d	⊢ ( 𝑧 = 𝑥 → ( ( 𝜓 → ¬ 𝑦 𝑅 𝑧 ) ↔ ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
12	11	ralbidv	⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
13	12	rexrab2	⊢ ( ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑧 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
14	8 13	bitri	⊢ ( ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ¬ 𝑦 𝑅 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
15	6 14	sylib	⊢ ( ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
16	15	an4s	⊢ ( ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∈ V ∧ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 ) ∧ ( 𝑅 Fr 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
17	4 5 16	mpanl12	⊢ ( ( 𝑅 Fr 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
18	17	ex	⊢ ( 𝑅 Fr 𝐴 → ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) ) )
19	3 18	syl5bir	⊢ ( 𝑅 Fr 𝐴 → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) ) )