Metamath Proof Explorer

Theorem bnj906

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj906 ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\right)\to pred\left({X},{A},{R}\right)\subseteq trCl\left({X},{A},{R}\right)$

Proof

Step Hyp Ref Expression
1 1onn ${⊢}{1}_{𝑜}\in \mathrm{\omega }$
2 1n0 ${⊢}{1}_{𝑜}\ne \varnothing$
3 eldifsn ${⊢}{1}_{𝑜}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)↔\left({1}_{𝑜}\in \mathrm{\omega }\wedge {1}_{𝑜}\ne \varnothing \right)$
4 1 2 3 mpbir2an ${⊢}{1}_{𝑜}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)$
5 4 ne0ii ${⊢}\mathrm{\omega }\setminus \left\{\varnothing \right\}\ne \varnothing$
6 biid ${⊢}{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)↔{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
7 biid ${⊢}\forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)↔\forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)$
8 eqid ${⊢}\mathrm{\omega }\setminus \left\{\varnothing \right\}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
9 6 7 8 bnj852 ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\right)\to \forall {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)$
10 r19.2z ${⊢}\left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\ne \varnothing \wedge \forall {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right)\to \exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)$
11 5 9 10 sylancr ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\right)\to \exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)$
12 euex ${⊢}\exists !{f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)$
13 11 12 bnj31 ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\right)\to \exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)$
14 rexcom4 ${⊢}\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)$
15 13 14 sylib ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)$
16 abid ${⊢}{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}↔\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)$
17 15 16 bnj1198 ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}$
18 simp2 ${⊢}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\to {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
19 18 reximi ${⊢}\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\to \exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
20 16 19 sylbi ${⊢}{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\to \exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
21 df-rex ${⊢}\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)↔\exists {n}\phantom{\rule{.4em}{0ex}}\left({n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\right)$
22 19.41v ${⊢}\exists {n}\phantom{\rule{.4em}{0ex}}\left({n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\right)↔\left(\exists {n}\phantom{\rule{.4em}{0ex}}{n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\right)$
23 22 simprbi ${⊢}\exists {n}\phantom{\rule{.4em}{0ex}}\left({n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\right)\to {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
24 21 23 sylbi ${⊢}\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\to {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
25 20 24 syl ${⊢}{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\to {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)$
26 eqid ${⊢}\left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}=\left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}$
27 8 26 bnj900 ${⊢}{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\to \varnothing \in \mathrm{dom}{f}$
28 fveq2 ${⊢}{i}=\varnothing \to {f}\left({i}\right)={f}\left(\varnothing \right)$
29 28 ssiun2s ${⊢}\varnothing \in \mathrm{dom}{f}\to {f}\left(\varnothing \right)\subseteq \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)$
30 27 29 syl ${⊢}{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\to {f}\left(\varnothing \right)\subseteq \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)$
31 ssiun2 ${⊢}{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\to \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\subseteq \bigcup _{{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)$
32 6 7 8 26 bnj882 ${⊢}trCl\left({X},{A},{R}\right)=\bigcup _{{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}}\bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)$
33 31 32 sseqtrrdi ${⊢}{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\to \bigcup _{{i}\in \mathrm{dom}{f}}{f}\left({i}\right)\subseteq trCl\left({X},{A},{R}\right)$
34 30 33 sstrd ${⊢}{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\to {f}\left(\varnothing \right)\subseteq trCl\left({X},{A},{R}\right)$
35 25 34 eqsstrrd ${⊢}{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\to pred\left({X},{A},{R}\right)\subseteq trCl\left({X},{A},{R}\right)$
36 35 exlimiv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left\{{f}|\exists {n}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {f}\left(\varnothing \right)=pred\left({X},{A},{R}\right)\wedge \forall {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{i}\in {n}\to {f}\left(\mathrm{suc}{i}\right)=\bigcup _{{y}\in {f}\left({i}\right)}pred\left({y},{A},{R}\right)\right)\right)\right\}\to pred\left({X},{A},{R}\right)\subseteq trCl\left({X},{A},{R}\right)$
37 17 36 syl ${⊢}\left({R}FrSe{A}\wedge {X}\in {A}\right)\to pred\left({X},{A},{R}\right)\subseteq trCl\left({X},{A},{R}\right)$