Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frind Structured version   Unicode version

Theorem frind 25523
 Description: The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin 25522). This principle states that if is a subclass of a founded class with the property that every element of whose initial segment is included in is itself equal to . Compare wfi 25487 and tfi 4836, which are special cases of this theorem that do not require the axiom of infinity to prove. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
Assertion
Ref Expression
frind Se
Distinct variable groups:   ,   ,   ,

Proof of Theorem frind
StepHypRef Expression
1 ssdif0 3688 . . . . . . 7
21necon3bbii 2634 . . . . . 6
3 difss 3476 . . . . . . 7
4 frmin 25522 . . . . . . . . 9 Se
5 eldif 3332 . . . . . . . . . . . . 13
65anbi1i 678 . . . . . . . . . . . 12
7 anass 632 . . . . . . . . . . . 12
8 ancom 439 . . . . . . . . . . . . . 14
9 indif2 3586 . . . . . . . . . . . . . . . . . 18
10 df-pred 25444 . . . . . . . . . . . . . . . . . . 19
11 incom 3535 . . . . . . . . . . . . . . . . . . 19
1210, 11eqtri 2458 . . . . . . . . . . . . . . . . . 18
13 df-pred 25444 . . . . . . . . . . . . . . . . . . . 20
14 incom 3535 . . . . . . . . . . . . . . . . . . . 20
1513, 14eqtri 2458 . . . . . . . . . . . . . . . . . . 19
1615difeq1i 3463 . . . . . . . . . . . . . . . . . 18
179, 12, 163eqtr4i 2468 . . . . . . . . . . . . . . . . 17
1817eqeq1i 2445 . . . . . . . . . . . . . . . 16
19 ssdif0 3688 . . . . . . . . . . . . . . . 16
2018, 19bitr4i 245 . . . . . . . . . . . . . . 15
2120anbi1i 678 . . . . . . . . . . . . . 14
228, 21bitri 242 . . . . . . . . . . . . 13
2322anbi2i 677 . . . . . . . . . . . 12
246, 7, 233bitri 264 . . . . . . . . . . 11
2524rexbii2 2736 . . . . . . . . . 10
26 rexanali 2753 . . . . . . . . . 10
2725, 26bitri 242 . . . . . . . . 9
284, 27sylib 190 . . . . . . . 8 Se
2928ex 425 . . . . . . 7 Se
303, 29mpani 659 . . . . . 6 Se
312, 30syl5bi 210 . . . . 5 Se
3231con4d 100 . . . 4 Se
3332imp 420 . . 3 Se