Theorem frindi

Description: The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin ). This principle states that if B is a subclass of a founded class A with the property that every element of B whose initial segment is included in A is itself equal to A . (Contributed by Scott Fenton, 6-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	frind.1	⊢ 𝑅 Fr 𝐴
	frind.2	⊢ 𝑅 Se 𝐴
Assertion	frindi	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		frind.1	⊢ 𝑅 Fr 𝐴
2		frind.2	⊢ 𝑅 Se 𝐴
3		frind	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) ) → 𝐴 = 𝐵 )
4	1 2 3	mpanl12	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) → 𝐴 = 𝐵 )