wfi

Description: The Principle of Well-Ordered Induction. Theorem 6.27 of TakeutiZaring p. 32. This principle states that if B is a subclass of a well-ordered class A with the property that every element of B whose inital segment is included in A is itself equal to A . (Contributed by Scott Fenton, 29-Jan-2011) (Revised by Mario Carneiro, 26-Jun-2015) (Proof shortened by Scott Fenton, 17-Nov-2024)

		Ref	Expression
	Assertion	wfi	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B))) \to A = B$

Proof

Step	Hyp	Ref	Expression
1		wefr	$⊢ R We A \to R Fr A$
2	1	adantr	$⊢ (R We A \land R Se A) \to R Fr A$
3		weso	$⊢ R We A \to R Or A$
4		sopo	$⊢ R Or A \to R Po A$
5	3 4	syl	$⊢ R We A \to R Po A$
6	5	adantr	$⊢ (R We A \land R Se A) \to R Po A$
7		simpr	$⊢ (R We A \land R Se A) \to R Se A$
8	2 6 7	3jca	$⊢ (R We A \land R Se A) \to (R Fr A \land R Po A \land R Se A)$
9		frpoind	$⊢ ((R Fr A \land R Po A \land R Se A) \land (B \subseteq A \land \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B))) \to A = B$
10	8 9	sylan	$⊢ ((R We A \land R Se A) \land (B \subseteq A \land \forall y \in A (Pred (R, A, y) \subseteq B \to y \in B))) \to A = B$

Metamath Proof Explorer

Theorem wfi

Proof