Metamath Proof Explorer

Theorem frind

Description: A subclass of a well-founded class A with the property that whenever it contains all predecessors of an element of A it also contains that element, is equal to A . Compare wfi and tfi , which are special cases of this theorem that do not require the axiom of infinity. (Contributed by Scott Fenton, 6-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion frind 
|- ( ( ( R Fr 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 frmin 
 |-  ( ( ( R Fr 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 ancom 
 |-  ( ( -. y e. B /\ Pred ( R , ( A \ B ) , y ) = (/) ) <-> ( Pred ( R , ( A \ B ) , y ) = (/) /\ -. y e. B ) )
9 indif2 
 |-  ( ( `' R " { y } ) i^i ( A \ B ) ) = ( ( ( `' R " { y } ) i^i A ) \ B )
10 df-pred 
 |-  Pred ( R , ( A \ B ) , y ) = ( ( A \ B ) i^i ( `' R " { y } ) )
11 incom 
 |-  ( ( A \ B ) i^i ( `' R " { y } ) ) = ( ( `' R " { y } ) i^i ( A \ B ) )
12 10 11 eqtri 
 |-  Pred ( R , ( A \ B ) , y ) = ( ( `' R " { y } ) i^i ( A \ B ) )
13 df-pred 
 |-  Pred ( R , A , y ) = ( A i^i ( `' R " { y } ) )
14 incom 
 |-  ( A i^i ( `' R " { y } ) ) = ( ( `' R " { y } ) i^i A )
15 13 14 eqtri 
 |-  Pred ( R , A , y ) = ( ( `' R " { y } ) i^i A )
16 15 difeq1i 
 |-  ( Pred ( R , A , y ) \ B ) = ( ( ( `' R " { y } ) i^i A ) \ B )
17 9 12 16 3eqtr4i 
 |-  Pred ( R , ( A \ B ) , y ) = ( Pred ( R , A , y ) \ B )
18 17 eqeq1i 
 |-  ( Pred ( R , ( A \ B ) , y ) = (/) <-> ( Pred ( R , A , y ) \ B ) = (/) )
19 ssdif0 
 |-  ( Pred ( R , A , y ) C_ B <-> ( Pred ( R , A , y ) \ B ) = (/) )
20 18 19 bitr4i 
 |-  ( Pred ( R , ( A \ B ) , y ) = (/) <-> Pred ( R , A , y ) C_ B )
21 20 anbi1i 
 |-  ( ( Pred ( R , ( A \ B ) , y ) = (/) /\ -. y e. B ) <-> ( Pred ( R , A , y ) C_ B /\ -. y e. B ) )
22 8 21 bitri 
 |-  ( ( -. y e. B /\ Pred ( R , ( A \ B ) , y ) = (/) ) <-> ( Pred ( R , A , y ) C_ B /\ -. y e. B ) )
23 22 anbi2i 
 |-  ( ( y e. A /\ ( -. y e. B /\ Pred ( R , ( A \ B ) , y ) = (/) ) ) <-> ( y e. A /\ ( Pred ( R , A , y ) C_ B /\ -. y e. B ) ) )
24 6 7 23 3bitri 
 |-  ( ( y e. ( A \ B ) /\ Pred ( R , ( A \ B ) , y ) = (/) ) <-> ( y e. A /\ ( Pred ( R , A , y ) C_ B /\ -. y e. B ) ) )
25 24 rexbii2 
 |-  ( E. y e. ( A \ B ) Pred ( R , ( A \ B ) , y ) = (/) <-> E. y e. A ( Pred ( R , A , y ) C_ B /\ -. y e. B ) )
26 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 ) )
27 25 26 bitri 
 |-  ( E. y e. ( A \ B ) Pred ( R , ( A \ B ) , y ) = (/) <-> -. A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) )
28 4 27 sylib 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( ( A \ B ) C_ A /\ ( A \ B ) =/= (/) ) ) -> -. A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) )
29 28 ex 
 |-  ( ( R Fr A /\ R Se A ) -> ( ( ( A \ B ) C_ A /\ ( A \ B ) =/= (/) ) -> -. A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) )
30 3 29 mpani 
 |-  ( ( R Fr A /\ R Se A ) -> ( ( A \ B ) =/= (/) -> -. A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) )
31 2 30 biimtrid 
 |-  ( ( R Fr A /\ R Se A ) -> ( -. A C_ B -> -. A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) )
32 31 con4d 
 |-  ( ( R Fr A /\ R Se A ) -> ( A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) -> A C_ B ) )
33 32 imp 
 |-  ( ( ( R Fr A /\ R Se A ) /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) -> A C_ B )
34 33 adantrl 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( B C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) ) -> A C_ B )
35 simprl 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( B C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) ) -> B C_ A )
36 34 35 eqssd 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( B C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) ) -> A = B )