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 C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) ) -> A = B )

Proof

Step Hyp Ref Expression
1 ssdif0 
 |-  ( A C_ B <-> ( A \ B ) = (/) )
2 1 necon3bbii 
 |-  ( -. A C_ B <-> ( A \ B ) =/= (/) )
3 difss 
 |-  ( A \ B ) C_ A
4 tz6.26 
 |-  ( ( ( R We A /\ R Se A ) /\ ( ( A \ B ) C_ A /\ ( A \ B ) =/= (/) ) ) -> E. y e. ( A \ B ) Pred ( R , ( A \ B ) , y ) = (/) )
5 eldif 
 |-  ( y e. ( A \ B ) <-> ( y e. A /\ -. y e. B ) )
6 5 anbi1i 
 |-  ( ( y e. ( A \ B ) /\ Pred ( R , ( A \ B ) , y ) = (/) ) <-> ( ( y e. A /\ -. y e. B ) /\ Pred ( R , ( A \ B ) , y ) = (/) ) )
7 anass 
 |-  ( ( ( y e. A /\ -. y e. B ) /\ Pred ( R , ( A \ B ) , y ) = (/) ) <-> ( y e. A /\ ( -. y e. B /\ Pred ( R , ( A \ B ) , y ) = (/) ) ) )
8 indif2 
 |-  ( ( `' R " { y } ) i^i ( A \ B ) ) = ( ( ( `' R " { y } ) i^i A ) \ B )
9 df-pred 
 |-  Pred ( R , ( A \ B ) , y ) = ( ( A \ B ) i^i ( `' R " { y } ) )
10 incom 
 |-  ( ( A \ B ) i^i ( `' R " { y } ) ) = ( ( `' R " { y } ) i^i ( A \ B ) )
11 9 10 eqtri 
 |-  Pred ( R , ( A \ B ) , y ) = ( ( `' R " { y } ) i^i ( A \ B ) )
12 df-pred 
 |-  Pred ( R , A , y ) = ( A i^i ( `' R " { y } ) )
13 incom 
 |-  ( A i^i ( `' R " { y } ) ) = ( ( `' R " { y } ) i^i A )
14 12 13 eqtri 
 |-  Pred ( R , A , y ) = ( ( `' R " { y } ) i^i A )
15 14 difeq1i 
 |-  ( Pred ( R , A , y ) \ B ) = ( ( ( `' R " { y } ) i^i 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 ) C_ B <-> ( Pred ( R , A , y ) \ B ) = (/) )
19 17 18 bitr4i 
 |-  ( Pred ( R , ( A \ B ) , y ) = (/) <-> Pred ( R , A , y ) C_ B )
20 19 anbi1ci 
 |-  ( ( -. y e. B /\ Pred ( R , ( A \ B ) , y ) = (/) ) <-> ( Pred ( R , A , y ) C_ B /\ -. y e. B ) )
21 20 anbi2i 
 |-  ( ( y e. A /\ ( -. y e. B /\ Pred ( R , ( A \ B ) , y ) = (/) ) ) <-> ( y e. A /\ ( Pred ( R , A , y ) C_ B /\ -. y e. B ) ) )
22 6 7 21 3bitri 
 |-  ( ( y e. ( A \ B ) /\ Pred ( R , ( A \ B ) , y ) = (/) ) <-> ( y e. A /\ ( Pred ( R , A , y ) C_ B /\ -. y e. B ) ) )
23 22 rexbii2 
 |-  ( E. y e. ( A \ B ) Pred ( R , ( A \ B ) , y ) = (/) <-> E. y e. A ( Pred ( R , A , y ) C_ B /\ -. y e. B ) )
24 rexanali 
 |-  ( E. y e. A ( Pred ( R , A , y ) C_ B /\ -. y e. B ) <-> -. A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) )
25 23 24 bitri 
 |-  ( E. y e. ( A \ B ) Pred ( R , ( A \ B ) , y ) = (/) <-> -. A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) )
26 4 25 sylib 
 |-  ( ( ( R We A /\ R Se A ) /\ ( ( A \ B ) C_ A /\ ( A \ B ) =/= (/) ) ) -> -. A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) )
27 26 ex 
 |-  ( ( R We A /\ R Se A ) -> ( ( ( A \ B ) C_ A /\ ( A \ B ) =/= (/) ) -> -. A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) )
28 3 27 mpani 
 |-  ( ( R We A /\ R Se A ) -> ( ( A \ B ) =/= (/) -> -. A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) )
29 2 28 syl5bi 
 |-  ( ( R We A /\ R Se A ) -> ( -. A C_ B -> -. A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) )
30 29 con4d 
 |-  ( ( R We A /\ R Se A ) -> ( A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) -> A C_ B ) )
31 30 imp 
 |-  ( ( ( R We A /\ R Se A ) /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) -> A C_ B )
32 31 adantrl 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) ) -> A C_ B )
33 simprl 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) ) -> B C_ A )
34 32 33 eqssd 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) ) -> A = B )