Metamath Proof Explorer


Theorem 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)

Ref Expression
Assertion wfi R We A R Se A B A y A Pred R A y B y B A = B

Proof

Step Hyp Ref Expression
1 ssdif0 A B A B =
2 1 necon3bbii ¬ A B A B
3 difss A B A
4 tz6.26 R We A R Se A A B A A B y A B Pred R A B y =
5 eldif y A B y A ¬ y B
6 5 anbi1i y A B Pred R A B y = y A ¬ y B Pred R A B y =
7 anass y A ¬ y B Pred R A B y = y A ¬ y B Pred R A B y =
8 indif2 R -1 y A B = R -1 y A B
9 df-pred Pred R A B y = A B R -1 y
10 incom A B R -1 y = R -1 y A B
11 9 10 eqtri Pred R A B y = R -1 y A B
12 df-pred Pred R A y = A R -1 y
13 incom A R -1 y = R -1 y A
14 12 13 eqtri Pred R A y = R -1 y A
15 14 difeq1i Pred R A y B = R -1 y A B
16 8 11 15 3eqtr4i Pred R A B y = Pred R A y B
17 16 eqeq1i Pred R A B y = Pred R A y B =
18 ssdif0 Pred R A y B Pred R A y B =
19 17 18 bitr4i Pred R A B y = Pred R A y B
20 19 anbi1ci ¬ y B Pred R A B y = Pred R A y B ¬ y B
21 20 anbi2i y A ¬ y B Pred R A B y = y A Pred R A y B ¬ y B
22 6 7 21 3bitri y A B Pred R A B y = y A Pred R A y B ¬ y B
23 22 rexbii2 y A B Pred R A B y = y A Pred R A y B ¬ y B
24 rexanali y A Pred R A y B ¬ y B ¬ y A Pred R A y B y B
25 23 24 bitri y A B Pred R A B y = ¬ y A Pred R A y B y B
26 4 25 sylib R We A R Se A A B A A B ¬ y A Pred R A y B y B
27 26 ex R We A R Se A A B A A B ¬ y A Pred R A y B y B
28 3 27 mpani R We A R Se A A B ¬ y A Pred R A y B y B
29 2 28 syl5bi R We A R Se A ¬ A B ¬ y A Pred R A y B y B
30 29 con4d R We A R Se A y A Pred R A y B y B A B
31 30 imp R We A R Se A y A Pred R A y B y B A B
32 31 adantrl R We A R Se A B A y A Pred R A y B y B A B
33 simprl R We A R Se A B A y A Pred R A y B y B B A
34 32 33 eqssd R We A R Se A B A y A Pred R A y B y B A = B