# Metamath Proof Explorer

## Theorem frpoind

Description: The principle of founded induction over a partial ordering. This theorem is a version of frind that does not require infinity, and can be used to prove wfi and tfi . (Contributed by Scott Fenton, 11-Feb-2022)

Ref Expression
Assertion frpoind ${⊢}\left(\left({R}\mathrm{Fr}{A}\wedge {R}\mathrm{Po}{A}\wedge {R}\mathrm{Se}{A}\right)\wedge \left({B}\subseteq {A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\to {y}\in {B}\right)\right)\right)\to {A}={B}$

### Proof

Step Hyp Ref Expression
1 ssdif0 ${⊢}{A}\subseteq {B}↔{A}\setminus {B}=\varnothing$
2 1 necon3bbii ${⊢}¬{A}\subseteq {B}↔{A}\setminus {B}\ne \varnothing$
3 difss ${⊢}{A}\setminus {B}\subseteq {A}$
4 frpomin2 ${⊢}\left(\left({R}\mathrm{Fr}{A}\wedge {R}\mathrm{Po}{A}\wedge {R}\mathrm{Se}{A}\right)\wedge \left({A}\setminus {B}\subseteq {A}\wedge {A}\setminus {B}\ne \varnothing \right)\right)\to \exists {y}\in \left({A}\setminus {B}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=\varnothing$
5 eldif ${⊢}{y}\in \left({A}\setminus {B}\right)↔\left({y}\in {A}\wedge ¬{y}\in {B}\right)$
6 5 anbi1i ${⊢}\left({y}\in \left({A}\setminus {B}\right)\wedge Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=\varnothing \right)↔\left(\left({y}\in {A}\wedge ¬{y}\in {B}\right)\wedge Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=\varnothing \right)$
7 anass ${⊢}\left(\left({y}\in {A}\wedge ¬{y}\in {B}\right)\wedge Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=\varnothing \right)↔\left({y}\in {A}\wedge \left(¬{y}\in {B}\wedge Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=\varnothing \right)\right)$
8 indif2 ${⊢}{{R}}^{-1}\left[\left\{{y}\right\}\right]\cap \left({A}\setminus {B}\right)=\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\cap {A}\right)\setminus {B}$
9 df-pred ${⊢}Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=\left({A}\setminus {B}\right)\cap {{R}}^{-1}\left[\left\{{y}\right\}\right]$
10 incom ${⊢}\left({A}\setminus {B}\right)\cap {{R}}^{-1}\left[\left\{{y}\right\}\right]={{R}}^{-1}\left[\left\{{y}\right\}\right]\cap \left({A}\setminus {B}\right)$
11 9 10 eqtri ${⊢}Pred\left({R},\left({A}\setminus {B}\right),{y}\right)={{R}}^{-1}\left[\left\{{y}\right\}\right]\cap \left({A}\setminus {B}\right)$
12 df-pred ${⊢}Pred\left({R},{A},{y}\right)={A}\cap {{R}}^{-1}\left[\left\{{y}\right\}\right]$
13 incom ${⊢}{A}\cap {{R}}^{-1}\left[\left\{{y}\right\}\right]={{R}}^{-1}\left[\left\{{y}\right\}\right]\cap {A}$
14 12 13 eqtri ${⊢}Pred\left({R},{A},{y}\right)={{R}}^{-1}\left[\left\{{y}\right\}\right]\cap {A}$
15 14 difeq1i ${⊢}Pred\left({R},{A},{y}\right)\setminus {B}=\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\cap {A}\right)\setminus {B}$
16 8 11 15 3eqtr4i ${⊢}Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=Pred\left({R},{A},{y}\right)\setminus {B}$
17 16 eqeq1i ${⊢}Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=\varnothing ↔Pred\left({R},{A},{y}\right)\setminus {B}=\varnothing$
18 ssdif0 ${⊢}Pred\left({R},{A},{y}\right)\subseteq {B}↔Pred\left({R},{A},{y}\right)\setminus {B}=\varnothing$
19 17 18 bitr4i ${⊢}Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=\varnothing ↔Pred\left({R},{A},{y}\right)\subseteq {B}$
20 19 anbi1ci ${⊢}\left(¬{y}\in {B}\wedge Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=\varnothing \right)↔\left(Pred\left({R},{A},{y}\right)\subseteq {B}\wedge ¬{y}\in {B}\right)$
21 20 anbi2i ${⊢}\left({y}\in {A}\wedge \left(¬{y}\in {B}\wedge Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=\varnothing \right)\right)↔\left({y}\in {A}\wedge \left(Pred\left({R},{A},{y}\right)\subseteq {B}\wedge ¬{y}\in {B}\right)\right)$
22 6 7 21 3bitri ${⊢}\left({y}\in \left({A}\setminus {B}\right)\wedge Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=\varnothing \right)↔\left({y}\in {A}\wedge \left(Pred\left({R},{A},{y}\right)\subseteq {B}\wedge ¬{y}\in {B}\right)\right)$
23 22 rexbii2 ${⊢}\exists {y}\in \left({A}\setminus {B}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=\varnothing ↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\wedge ¬{y}\in {B}\right)$
24 rexanali ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\wedge ¬{y}\in {B}\right)↔¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\to {y}\in {B}\right)$
25 23 24 bitri ${⊢}\exists {y}\in \left({A}\setminus {B}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},\left({A}\setminus {B}\right),{y}\right)=\varnothing ↔¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\to {y}\in {B}\right)$
26 4 25 sylib ${⊢}\left(\left({R}\mathrm{Fr}{A}\wedge {R}\mathrm{Po}{A}\wedge {R}\mathrm{Se}{A}\right)\wedge \left({A}\setminus {B}\subseteq {A}\wedge {A}\setminus {B}\ne \varnothing \right)\right)\to ¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\to {y}\in {B}\right)$
27 26 ex ${⊢}\left({R}\mathrm{Fr}{A}\wedge {R}\mathrm{Po}{A}\wedge {R}\mathrm{Se}{A}\right)\to \left(\left({A}\setminus {B}\subseteq {A}\wedge {A}\setminus {B}\ne \varnothing \right)\to ¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\to {y}\in {B}\right)\right)$
28 3 27 mpani ${⊢}\left({R}\mathrm{Fr}{A}\wedge {R}\mathrm{Po}{A}\wedge {R}\mathrm{Se}{A}\right)\to \left({A}\setminus {B}\ne \varnothing \to ¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\to {y}\in {B}\right)\right)$
29 2 28 syl5bi ${⊢}\left({R}\mathrm{Fr}{A}\wedge {R}\mathrm{Po}{A}\wedge {R}\mathrm{Se}{A}\right)\to \left(¬{A}\subseteq {B}\to ¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\to {y}\in {B}\right)\right)$
30 29 con4d ${⊢}\left({R}\mathrm{Fr}{A}\wedge {R}\mathrm{Po}{A}\wedge {R}\mathrm{Se}{A}\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\to {y}\in {B}\right)\to {A}\subseteq {B}\right)$
31 30 imp ${⊢}\left(\left({R}\mathrm{Fr}{A}\wedge {R}\mathrm{Po}{A}\wedge {R}\mathrm{Se}{A}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\to {y}\in {B}\right)\right)\to {A}\subseteq {B}$
32 31 adantrl ${⊢}\left(\left({R}\mathrm{Fr}{A}\wedge {R}\mathrm{Po}{A}\wedge {R}\mathrm{Se}{A}\right)\wedge \left({B}\subseteq {A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\to {y}\in {B}\right)\right)\right)\to {A}\subseteq {B}$
33 simprl ${⊢}\left(\left({R}\mathrm{Fr}{A}\wedge {R}\mathrm{Po}{A}\wedge {R}\mathrm{Se}{A}\right)\wedge \left({B}\subseteq {A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\to {y}\in {B}\right)\right)\right)\to {B}\subseteq {A}$
34 32 33 eqssd ${⊢}\left(\left({R}\mathrm{Fr}{A}\wedge {R}\mathrm{Po}{A}\wedge {R}\mathrm{Se}{A}\right)\wedge \left({B}\subseteq {A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(Pred\left({R},{A},{y}\right)\subseteq {B}\to {y}\in {B}\right)\right)\right)\to {A}={B}$