Theorem fri

Description: Property of well-founded relation (one direction of definition). (Contributed by NM, 18-Mar-1997)

	Ref	Expression
Assertion	fri	⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		df-fr	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ) )
2		sseq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
3		neeq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 ≠ ∅ ↔ 𝐵 ≠ ∅ ) )
4	2 3	anbi12d	⊢ ( 𝑧 = 𝐵 → ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) ↔ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) )
5		raleq	⊢ ( 𝑧 = 𝐵 → ( ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
6	5	rexeqbi1dv	⊢ ( 𝑧 = 𝐵 → ( ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
7	4 6	imbi12d	⊢ ( 𝑧 = 𝐵 → ( ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ) ↔ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ) )
8	7	spcgv	⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ) → ( ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ) )
9	1 8	syl5bi	⊢ ( 𝐵 ∈ 𝐶 → ( 𝑅 Fr 𝐴 → ( ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ) )
10	9	imp31	⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )