# Metamath Proof Explorer

## Theorem dfon2lem7

Description: Lemma for dfon2 . All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011)

Ref Expression
Hypothesis dfon2lem7.1 ${⊢}{A}\in \mathrm{V}$
Assertion dfon2lem7 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {A}\wedge \mathrm{Tr}{x}\right)\to {x}\in {A}\right)\to \left({B}\in {A}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {B}\wedge \mathrm{Tr}{y}\right)\to {y}\in {B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 dfon2lem7.1 ${⊢}{A}\in \mathrm{V}$
2 elequ1 ${⊢}{t}={z}\to \left({t}\in {t}↔{z}\in {t}\right)$
3 elequ2 ${⊢}{t}={z}\to \left({z}\in {t}↔{z}\in {z}\right)$
4 2 3 bitrd ${⊢}{t}={z}\to \left({t}\in {t}↔{z}\in {z}\right)$
5 4 notbid ${⊢}{t}={z}\to \left(¬{t}\in {t}↔¬{z}\in {z}\right)$
6 5 cbvralvw ${⊢}\forall {t}\in {x}\phantom{\rule{.4em}{0ex}}¬{t}\in {t}↔\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}¬{z}\in {z}$
7 6 biimpi ${⊢}\forall {t}\in {x}\phantom{\rule{.4em}{0ex}}¬{t}\in {t}\to \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}¬{z}\in {z}$
8 7 ralimi ${⊢}\forall {x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\forall {t}\in {x}\phantom{\rule{.4em}{0ex}}¬{t}\in {t}\to \forall {x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}¬{z}\in {z}$
9 untuni ${⊢}\forall {z}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}¬{z}\in {z}↔\forall {x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}¬{z}\in {z}$
10 8 9 sylibr ${⊢}\forall {x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\forall {t}\in {x}\phantom{\rule{.4em}{0ex}}¬{t}\in {t}\to \forall {z}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}¬{z}\in {z}$
11 vex ${⊢}{x}\in \mathrm{V}$
12 sseq1 ${⊢}{w}={x}\to \left({w}\subseteq {A}↔{x}\subseteq {A}\right)$
13 treq ${⊢}{w}={x}\to \left(\mathrm{Tr}{w}↔\mathrm{Tr}{x}\right)$
14 raleq ${⊢}{w}={x}\to \left(\forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)↔\forall {t}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)$
15 12 13 14 3anbi123d ${⊢}{w}={x}\to \left(\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)↔\left({x}\subseteq {A}\wedge \mathrm{Tr}{x}\wedge \forall {t}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right)$
16 11 15 elab ${⊢}{x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}↔\left({x}\subseteq {A}\wedge \mathrm{Tr}{x}\wedge \forall {t}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)$
17 vex ${⊢}{t}\in \mathrm{V}$
18 dfon2lem3 ${⊢}{t}\in \mathrm{V}\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\to \left(\mathrm{Tr}{t}\wedge \forall {u}\in {t}\phantom{\rule{.4em}{0ex}}¬{u}\in {u}\right)\right)$
19 17 18 ax-mp ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\to \left(\mathrm{Tr}{t}\wedge \forall {u}\in {t}\phantom{\rule{.4em}{0ex}}¬{u}\in {u}\right)$
20 19 simprd ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\to \forall {u}\in {t}\phantom{\rule{.4em}{0ex}}¬{u}\in {u}$
21 untelirr ${⊢}\forall {u}\in {t}\phantom{\rule{.4em}{0ex}}¬{u}\in {u}\to ¬{t}\in {t}$
22 20 21 syl ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\to ¬{t}\in {t}$
23 22 ralimi ${⊢}\forall {t}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\to \forall {t}\in {x}\phantom{\rule{.4em}{0ex}}¬{t}\in {t}$
24 23 3ad2ant3 ${⊢}\left({x}\subseteq {A}\wedge \mathrm{Tr}{x}\wedge \forall {t}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\to \forall {t}\in {x}\phantom{\rule{.4em}{0ex}}¬{t}\in {t}$
25 16 24 sylbi ${⊢}{x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \forall {t}\in {x}\phantom{\rule{.4em}{0ex}}¬{t}\in {t}$
26 10 25 mprg ${⊢}\forall {z}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}¬{z}\in {z}$
27 untelirr ${⊢}\forall {z}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}¬{z}\in {z}\to ¬\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}$
28 psseq2 ${⊢}{t}={u}\to \left({y}\subset {t}↔{y}\subset {u}\right)$
29 28 anbi1d ${⊢}{t}={u}\to \left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)↔\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\right)$
30 elequ2 ${⊢}{t}={u}\to \left({y}\in {t}↔{y}\in {u}\right)$
31 29 30 imbi12d ${⊢}{t}={u}\to \left(\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)↔\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)$
32 31 albidv ${⊢}{t}={u}\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)$
33 32 cbvralvw ${⊢}\forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)↔\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)$
34 33 3anbi3i ${⊢}\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)↔\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)$
35 34 abbii ${⊢}\left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}=\left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}$
36 35 unieqi ${⊢}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}$
37 36 eleq2i ${⊢}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}↔\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}$
38 27 37 sylnib ${⊢}\forall {z}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}¬{z}\in {z}\to ¬\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}$
39 26 38 ax-mp ${⊢}¬\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}$
40 dfon2lem2 ${⊢}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}$
41 1 40 ssexi ${⊢}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in \mathrm{V}$
42 41 snss ${⊢}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}↔\left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}$
43 39 42 mtbi ${⊢}¬\left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}$
44 43 intnan ${⊢}¬\left(\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}\wedge \left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}\right)$
45 df-suc ${⊢}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\cup \left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}$
46 45 sseq1i ${⊢}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}↔\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\cup \left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}$
47 unss ${⊢}\left(\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}\wedge \left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}\right)↔\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\cup \left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}$
48 46 47 bitr4i ${⊢}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}↔\left(\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}\wedge \left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}\right)$
49 44 48 mtbir ${⊢}¬\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}$
50 41 snss ${⊢}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in {A}↔\left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq {A}$
51 45 sseq1i ${⊢}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}↔\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\cup \left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq {A}$
52 unss ${⊢}\left(\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}\wedge \left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq {A}\right)↔\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\cup \left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq {A}$
53 51 52 bitr4i ${⊢}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}↔\left(\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}\wedge \left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq {A}\right)$
54 dfon2lem1 ${⊢}\mathrm{Tr}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}$
55 suctr ${⊢}\mathrm{Tr}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \mathrm{Tr}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}$
56 54 55 ax-mp ${⊢}\mathrm{Tr}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}$
57 vex ${⊢}{u}\in \mathrm{V}$
58 57 elsuc ${⊢}{u}\in \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}↔\left({u}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\vee {u}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right)$
59 eluni2 ${⊢}{u}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}↔\exists {x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{u}\in {x}$
60 nfa1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)$
61 32 rspccv ${⊢}\forall {t}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\to \left({u}\in {x}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)$
62 psseq1 ${⊢}{y}={x}\to \left({y}\subset {u}↔{x}\subset {u}\right)$
63 treq ${⊢}{y}={x}\to \left(\mathrm{Tr}{y}↔\mathrm{Tr}{x}\right)$
64 62 63 anbi12d ${⊢}{y}={x}\to \left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)↔\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\right)$
65 elequ1 ${⊢}{y}={x}\to \left({y}\in {u}↔{x}\in {u}\right)$
66 64 65 imbi12d ${⊢}{y}={x}\to \left(\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)↔\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)$
67 66 cbvalvw ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)$
68 61 67 syl6ib ${⊢}\forall {t}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\to \left({u}\in {x}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)$
69 68 3ad2ant3 ${⊢}\left({x}\subseteq {A}\wedge \mathrm{Tr}{x}\wedge \forall {t}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\to \left({u}\in {x}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)$
70 16 69 sylbi ${⊢}{x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left({u}\in {x}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)$
71 60 70 rexlimi ${⊢}\exists {x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{u}\in {x}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)$
72 59 71 sylbi ${⊢}{u}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)$
73 psseq1 ${⊢}{y}={z}\to \left({y}\subset {u}↔{z}\subset {u}\right)$
74 treq ${⊢}{y}={z}\to \left(\mathrm{Tr}{y}↔\mathrm{Tr}{z}\right)$
75 73 74 anbi12d ${⊢}{y}={z}\to \left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)↔\left({z}\subset {u}\wedge \mathrm{Tr}{z}\right)\right)$
76 elequ1 ${⊢}{y}={z}\to \left({y}\in {u}↔{z}\in {u}\right)$
77 75 76 imbi12d ${⊢}{y}={z}\to \left(\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)↔\left(\left({z}\subset {u}\wedge \mathrm{Tr}{z}\right)\to {z}\in {u}\right)\right)$
78 77 cbvalvw ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\subset {u}\wedge \mathrm{Tr}{z}\right)\to {z}\in {u}\right)$
79 61 78 syl6ib ${⊢}\forall {t}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\to \left({u}\in {x}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\subset {u}\wedge \mathrm{Tr}{z}\right)\to {z}\in {u}\right)\right)$
80 79 3ad2ant3 ${⊢}\left({x}\subseteq {A}\wedge \mathrm{Tr}{x}\wedge \forall {t}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\to \left({u}\in {x}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\subset {u}\wedge \mathrm{Tr}{z}\right)\to {z}\in {u}\right)\right)$
81 16 80 sylbi ${⊢}{x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left({u}\in {x}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\subset {u}\wedge \mathrm{Tr}{z}\right)\to {z}\in {u}\right)\right)$
82 81 rexlimiv ${⊢}\exists {x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{u}\in {x}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\subset {u}\wedge \mathrm{Tr}{z}\right)\to {z}\in {u}\right)$
83 59 82 sylbi ${⊢}{u}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\subset {u}\wedge \mathrm{Tr}{z}\right)\to {z}\in {u}\right)$
84 83 rgen ${⊢}\forall {u}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\subset {u}\wedge \mathrm{Tr}{z}\right)\to {z}\in {u}\right)$
85 dfon2lem6 ${⊢}\left(\mathrm{Tr}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\wedge \forall {u}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\subset {u}\wedge \mathrm{Tr}{z}\right)\to {z}\in {u}\right)\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\wedge \mathrm{Tr}{x}\right)\to {x}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right)$
86 54 84 85 mp2an ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\wedge \mathrm{Tr}{x}\right)\to {x}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right)$
87 psseq2 ${⊢}{u}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left({x}\subset {u}↔{x}\subset \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right)$
88 87 anbi1d ${⊢}{u}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)↔\left({x}\subset \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\wedge \mathrm{Tr}{x}\right)\right)$
89 eleq2 ${⊢}{u}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left({x}\in {u}↔{x}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right)$
90 88 89 imbi12d ${⊢}{u}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left(\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)↔\left(\left({x}\subset \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\wedge \mathrm{Tr}{x}\right)\to {x}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right)\right)$
91 90 albidv ${⊢}{u}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\wedge \mathrm{Tr}{x}\right)\to {x}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right)\right)$
92 86 91 mpbiri ${⊢}{u}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)$
93 72 92 jaoi ${⊢}\left({u}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\vee {u}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)$
94 58 93 sylbi ${⊢}{u}\in \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)$
95 94 rgen ${⊢}\forall {u}\in \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)$
96 41 sucex ${⊢}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in \mathrm{V}$
97 sseq1 ${⊢}{s}=\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left({s}\subseteq {A}↔\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}\right)$
98 treq ${⊢}{s}=\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left(\mathrm{Tr}{s}↔\mathrm{Tr}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right)$
99 raleq ${⊢}{s}=\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left(\forall {u}\in {s}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)↔\forall {u}\in \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)$
100 97 98 99 3anbi123d ${⊢}{s}=\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left(\left({s}\subseteq {A}\wedge \mathrm{Tr}{s}\wedge \forall {u}\in {s}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)↔\left(\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}\wedge \mathrm{Tr}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\wedge \forall {u}\in \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)\right)$
101 96 100 elab ${⊢}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in \left\{{s}|\left({s}\subseteq {A}\wedge \mathrm{Tr}{s}\wedge \forall {u}\in {s}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)\right\}↔\left(\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}\wedge \mathrm{Tr}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\wedge \forall {u}\in \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)$
102 elssuni ${⊢}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in \left\{{s}|\left({s}\subseteq {A}\wedge \mathrm{Tr}{s}\wedge \forall {u}\in {s}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)\right\}\to \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{s}|\left({s}\subseteq {A}\wedge \mathrm{Tr}{s}\wedge \forall {u}\in {s}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)\right\}$
103 101 102 sylbir ${⊢}\left(\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}\wedge \mathrm{Tr}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\wedge \forall {u}\in \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)\to \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{s}|\left({s}\subseteq {A}\wedge \mathrm{Tr}{s}\wedge \forall {u}\in {s}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)\right\}$
104 56 95 103 mp3an23 ${⊢}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}\to \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{s}|\left({s}\subseteq {A}\wedge \mathrm{Tr}{s}\wedge \forall {u}\in {s}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)\right\}$
105 sseq1 ${⊢}{s}={w}\to \left({s}\subseteq {A}↔{w}\subseteq {A}\right)$
106 treq ${⊢}{s}={w}\to \left(\mathrm{Tr}{s}↔\mathrm{Tr}{w}\right)$
107 raleq ${⊢}{s}={w}\to \left(\forall {u}\in {s}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)↔\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)$
108 psseq1 ${⊢}{x}={y}\to \left({x}\subset {u}↔{y}\subset {u}\right)$
109 treq ${⊢}{x}={y}\to \left(\mathrm{Tr}{x}↔\mathrm{Tr}{y}\right)$
110 108 109 anbi12d ${⊢}{x}={y}\to \left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)↔\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\right)$
111 elequ1 ${⊢}{x}={y}\to \left({x}\in {u}↔{y}\in {u}\right)$
112 110 111 imbi12d ${⊢}{x}={y}\to \left(\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)↔\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)$
113 112 cbvalvw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)$
114 113 ralbii ${⊢}\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)↔\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)$
115 107 114 syl6bb ${⊢}{s}={w}\to \left(\forall {u}\in {s}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)↔\forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)$
116 105 106 115 3anbi123d ${⊢}{s}={w}\to \left(\left({s}\subseteq {A}\wedge \mathrm{Tr}{s}\wedge \forall {u}\in {s}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)↔\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right)$
117 116 cbvabv ${⊢}\left\{{s}|\left({s}\subseteq {A}\wedge \mathrm{Tr}{s}\wedge \forall {u}\in {s}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)\right\}=\left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}$
118 117 unieqi ${⊢}\bigcup \left\{{s}|\left({s}\subseteq {A}\wedge \mathrm{Tr}{s}\wedge \forall {u}\in {s}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {u}\wedge \mathrm{Tr}{x}\right)\to {x}\in {u}\right)\right)\right\}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}$
119 104 118 sseqtrdi ${⊢}\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}\to \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}$
120 119 a1i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {A}\wedge \mathrm{Tr}{x}\right)\to {x}\in {A}\right)\to \left(\mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}\to \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}\right)$
121 53 120 syl5bir ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {A}\wedge \mathrm{Tr}{x}\right)\to {x}\in {A}\right)\to \left(\left(\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}\wedge \left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq {A}\right)\to \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}\right)$
122 40 121 mpani ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {A}\wedge \mathrm{Tr}{x}\right)\to {x}\in {A}\right)\to \left(\left\{\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right\}\subseteq {A}\to \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}\right)$
123 50 122 syl5bi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {A}\wedge \mathrm{Tr}{x}\right)\to {x}\in {A}\right)\to \left(\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in {A}\to \mathrm{suc}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {u}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {u}\wedge \mathrm{Tr}{y}\right)\to {y}\in {u}\right)\right)\right\}\right)$
124 49 123 mtoi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {A}\wedge \mathrm{Tr}{x}\right)\to {x}\in {A}\right)\to ¬\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in {A}$
125 psseq1 ${⊢}{x}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left({x}\subset {A}↔\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subset {A}\right)$
126 treq ${⊢}{x}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left(\mathrm{Tr}{x}↔\mathrm{Tr}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right)$
127 125 126 anbi12d ${⊢}{x}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left(\left({x}\subset {A}\wedge \mathrm{Tr}{x}\right)↔\left(\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subset {A}\wedge \mathrm{Tr}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right)\right)$
128 eleq1 ${⊢}{x}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left({x}\in {A}↔\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in {A}\right)$
129 127 128 imbi12d ${⊢}{x}=\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left(\left(\left({x}\subset {A}\wedge \mathrm{Tr}{x}\right)\to {x}\in {A}\right)↔\left(\left(\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subset {A}\wedge \mathrm{Tr}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right)\to \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in {A}\right)\right)$
130 41 129 spcv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {A}\wedge \mathrm{Tr}{x}\right)\to {x}\in {A}\right)\to \left(\left(\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subset {A}\wedge \mathrm{Tr}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\right)\to \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in {A}\right)$
131 54 130 mpan2i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {A}\wedge \mathrm{Tr}{x}\right)\to {x}\in {A}\right)\to \left(\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subset {A}\to \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\in {A}\right)$
132 124 131 mtod ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {A}\wedge \mathrm{Tr}{x}\right)\to {x}\in {A}\right)\to ¬\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subset {A}$
133 dfpss2 ${⊢}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subset {A}↔\left(\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}\wedge ¬\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}={A}\right)$
134 133 biimpri ${⊢}\left(\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subseteq {A}\wedge ¬\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}={A}\right)\to \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subset {A}$
135 40 134 mpan ${⊢}¬\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}={A}\to \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\subset {A}$
136 132 135 nsyl2 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {A}\wedge \mathrm{Tr}{x}\right)\to {x}\in {A}\right)\to \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}={A}$
137 eluni2 ${⊢}{z}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}↔\exists {x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\in {x}$
138 psseq2 ${⊢}{t}={z}\to \left({y}\subset {t}↔{y}\subset {z}\right)$
139 138 anbi1d ${⊢}{t}={z}\to \left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)↔\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\right)$
140 elequ2 ${⊢}{t}={z}\to \left({y}\in {t}↔{y}\in {z}\right)$
141 139 140 imbi12d ${⊢}{t}={z}\to \left(\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)↔\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)\right)$
142 141 albidv ${⊢}{t}={z}\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)\right)$
143 142 cbvralvw ${⊢}\forall {t}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)↔\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)$
144 14 143 syl6bb ${⊢}{w}={x}\to \left(\forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)↔\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)\right)$
145 12 13 144 3anbi123d ${⊢}{w}={x}\to \left(\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)↔\left({x}\subseteq {A}\wedge \mathrm{Tr}{x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)\right)\right)$
146 11 145 elab ${⊢}{x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}↔\left({x}\subseteq {A}\wedge \mathrm{Tr}{x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)\right)$
147 rsp ${⊢}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)\to \left({z}\in {x}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)\right)$
148 147 3ad2ant3 ${⊢}\left({x}\subseteq {A}\wedge \mathrm{Tr}{x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)\right)\to \left({z}\in {x}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)\right)$
149 146 148 sylbi ${⊢}{x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \left({z}\in {x}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)\right)$
150 149 rexlimiv ${⊢}\exists {x}\in \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\in {x}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)$
151 137 150 sylbi ${⊢}{z}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)$
152 151 rgen ${⊢}\forall {z}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)$
153 raleq ${⊢}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}={A}\to \left(\forall {z}\in \bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)\right)$
154 152 153 mpbii ${⊢}\bigcup \left\{{w}|\left({w}\subseteq {A}\wedge \mathrm{Tr}{w}\wedge \forall {t}\in {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {t}\wedge \mathrm{Tr}{y}\right)\to {y}\in {t}\right)\right)\right\}={A}\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)$
155 psseq2 ${⊢}{z}={B}\to \left({y}\subset {z}↔{y}\subset {B}\right)$
156 155 anbi1d ${⊢}{z}={B}\to \left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)↔\left({y}\subset {B}\wedge \mathrm{Tr}{y}\right)\right)$
157 eleq2 ${⊢}{z}={B}\to \left({y}\in {z}↔{y}\in {B}\right)$
158 156 157 imbi12d ${⊢}{z}={B}\to \left(\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)↔\left(\left({y}\subset {B}\wedge \mathrm{Tr}{y}\right)\to {y}\in {B}\right)\right)$
159 158 albidv ${⊢}{z}={B}\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {B}\wedge \mathrm{Tr}{y}\right)\to {y}\in {B}\right)\right)$
160 159 rspccv ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {z}\wedge \mathrm{Tr}{y}\right)\to {y}\in {z}\right)\to \left({B}\in {A}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {B}\wedge \mathrm{Tr}{y}\right)\to {y}\in {B}\right)\right)$
161 136 154 160 3syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subset {A}\wedge \mathrm{Tr}{x}\right)\to {x}\in {A}\right)\to \left({B}\in {A}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\subset {B}\wedge \mathrm{Tr}{y}\right)\to {y}\in {B}\right)\right)$