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 /\ R Se A ) /\ ( B C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) ) -> A = B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wefr | |- ( R We A -> R Fr A ) |
|
2 | 1 | adantr | |- ( ( R We A /\ R Se A ) -> R Fr A ) |
3 | weso | |- ( R We A -> R Or A ) |
|
4 | sopo | |- ( R Or A -> R Po A ) |
|
5 | 3 4 | syl | |- ( R We A -> R Po A ) |
6 | 5 | adantr | |- ( ( R We A /\ R Se A ) -> R Po A ) |
7 | simpr | |- ( ( R We A /\ R Se A ) -> R Se A ) |
|
8 | 2 6 7 | 3jca | |- ( ( R We A /\ R Se A ) -> ( R Fr A /\ R Po A /\ R Se A ) ) |
9 | frpoind | |- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) ) -> A = B ) |
|
10 | 8 9 | sylan | |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) ) -> A = B ) |