# Metamath Proof Explorer

## Theorem f1otrg

Description: A bijection between bases which conserves distances and intervals conserves also geometries. (Contributed by Thierry Arnoux, 23-Mar-2019)

Ref Expression
Hypotheses f1otrkg.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
f1otrkg.d ${⊢}{D}=\mathrm{dist}\left({G}\right)$
f1otrkg.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
f1otrkg.b ${⊢}{B}={\mathrm{Base}}_{{H}}$
f1otrkg.e ${⊢}{E}=\mathrm{dist}\left({H}\right)$
f1otrkg.j ${⊢}{J}=\mathrm{Itv}\left({H}\right)$
f1otrkg.f ${⊢}{\phi }\to {F}:{B}\underset{1-1 onto}{⟶}{P}$
f1otrkg.1 ${⊢}\left({\phi }\wedge \left({e}\in {B}\wedge {f}\in {B}\right)\right)\to {e}{E}{f}={F}\left({e}\right){D}{F}\left({f}\right)$
f1otrkg.2 ${⊢}\left({\phi }\wedge \left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\right)\to \left({g}\in \left({e}{J}{f}\right)↔{F}\left({g}\right)\in \left({F}\left({e}\right){I}{F}\left({f}\right)\right)\right)$
f1otrg.h ${⊢}{\phi }\to {H}\in {V}$
f1otrg.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
f1otrg.l ${⊢}{\phi }\to {Line}_{𝒢}\left({H}\right)=\left({x}\in {B},{y}\in \left({B}\setminus \left\{{x}\right\}\right)⟼\left\{{z}\in {B}|\left({z}\in \left({x}{J}{y}\right)\vee {x}\in \left({z}{J}{y}\right)\vee {y}\in \left({x}{J}{z}\right)\right)\right\}\right)$
Assertion f1otrg ${⊢}{\phi }\to {H}\in {𝒢}_{\mathrm{Tarski}}$

### Proof

Step Hyp Ref Expression
1 f1otrkg.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 f1otrkg.d ${⊢}{D}=\mathrm{dist}\left({G}\right)$
3 f1otrkg.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
4 f1otrkg.b ${⊢}{B}={\mathrm{Base}}_{{H}}$
5 f1otrkg.e ${⊢}{E}=\mathrm{dist}\left({H}\right)$
6 f1otrkg.j ${⊢}{J}=\mathrm{Itv}\left({H}\right)$
7 f1otrkg.f ${⊢}{\phi }\to {F}:{B}\underset{1-1 onto}{⟶}{P}$
8 f1otrkg.1 ${⊢}\left({\phi }\wedge \left({e}\in {B}\wedge {f}\in {B}\right)\right)\to {e}{E}{f}={F}\left({e}\right){D}{F}\left({f}\right)$
9 f1otrkg.2 ${⊢}\left({\phi }\wedge \left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\right)\to \left({g}\in \left({e}{J}{f}\right)↔{F}\left({g}\right)\in \left({F}\left({e}\right){I}{F}\left({f}\right)\right)\right)$
10 f1otrg.h ${⊢}{\phi }\to {H}\in {V}$
11 f1otrg.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
12 f1otrg.l ${⊢}{\phi }\to {Line}_{𝒢}\left({H}\right)=\left({x}\in {B},{y}\in \left({B}\setminus \left\{{x}\right\}\right)⟼\left\{{z}\in {B}|\left({z}\in \left({x}{J}{y}\right)\vee {x}\in \left({z}{J}{y}\right)\vee {y}\in \left({x}{J}{z}\right)\right)\right\}\right)$
13 10 elexd ${⊢}{\phi }\to {H}\in \mathrm{V}$
14 11 adantr ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
15 f1of ${⊢}{F}:{B}\underset{1-1 onto}{⟶}{P}\to {F}:{B}⟶{P}$
16 7 15 syl ${⊢}{\phi }\to {F}:{B}⟶{P}$
17 16 adantr ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {F}:{B}⟶{P}$
18 simprl ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}\in {B}$
19 17 18 ffvelrnd ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {F}\left({x}\right)\in {P}$
20 simprr ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {y}\in {B}$
21 17 20 ffvelrnd ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {F}\left({y}\right)\in {P}$
22 1 2 3 14 19 21 axtgcgrrflx ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {F}\left({x}\right){D}{F}\left({y}\right)={F}\left({y}\right){D}{F}\left({x}\right)$
23 7 adantr ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {F}:{B}\underset{1-1 onto}{⟶}{P}$
24 8 adantlr ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\right)\right)\to {e}{E}{f}={F}\left({e}\right){D}{F}\left({f}\right)$
25 9 adantlr ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\right)\to \left({g}\in \left({e}{J}{f}\right)↔{F}\left({g}\right)\in \left({F}\left({e}\right){I}{F}\left({f}\right)\right)\right)$
26 1 2 3 4 5 6 23 24 25 18 20 f1otrgds ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{E}{y}={F}\left({x}\right){D}{F}\left({y}\right)$
27 1 2 3 4 5 6 23 24 25 20 18 f1otrgds ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {y}{E}{x}={F}\left({y}\right){D}{F}\left({x}\right)$
28 22 26 27 3eqtr4d ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{E}{y}={y}{E}{x}$
29 28 ralrimivva ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{E}{y}={y}{E}{x}$
30 f1of1 ${⊢}{F}:{B}\underset{1-1 onto}{⟶}{P}\to {F}:{B}\underset{1-1}{⟶}{P}$
31 7 30 syl ${⊢}{\phi }\to {F}:{B}\underset{1-1}{⟶}{P}$
32 31 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {F}:{B}\underset{1-1}{⟶}{P}$
33 simp21 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {x}\in {B}$
34 simp22 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {y}\in {B}$
35 33 34 jca ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to \left({x}\in {B}\wedge {y}\in {B}\right)$
36 11 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
37 16 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {F}:{B}⟶{P}$
38 37 33 ffvelrnd ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {F}\left({x}\right)\in {P}$
39 37 34 ffvelrnd ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {F}\left({y}\right)\in {P}$
40 simp23 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {z}\in {B}$
41 37 40 ffvelrnd ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {F}\left({z}\right)\in {P}$
42 simp3 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {x}{E}{y}={z}{E}{z}$
43 7 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {F}:{B}\underset{1-1 onto}{⟶}{P}$
44 8 3ad2antl1 ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\right)\right)\to {e}{E}{f}={F}\left({e}\right){D}{F}\left({f}\right)$
45 9 3ad2antl1 ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\right)\to \left({g}\in \left({e}{J}{f}\right)↔{F}\left({g}\right)\in \left({F}\left({e}\right){I}{F}\left({f}\right)\right)\right)$
46 1 2 3 4 5 6 43 44 45 33 34 f1otrgds ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {x}{E}{y}={F}\left({x}\right){D}{F}\left({y}\right)$
47 1 2 3 4 5 6 43 44 45 40 40 f1otrgds ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {z}{E}{z}={F}\left({z}\right){D}{F}\left({z}\right)$
48 42 46 47 3eqtr3d ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {F}\left({x}\right){D}{F}\left({y}\right)={F}\left({z}\right){D}{F}\left({z}\right)$
49 1 2 3 36 38 39 41 48 axtgcgrid ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {F}\left({x}\right)={F}\left({y}\right)$
50 f1veqaeq ${⊢}\left({F}:{B}\underset{1-1}{⟶}{P}\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)$
51 50 imp ${⊢}\left(\left({F}:{B}\underset{1-1}{⟶}{P}\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge {F}\left({x}\right)={F}\left({y}\right)\right)\to {x}={y}$
52 32 35 49 51 syl21anc ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\wedge {x}{E}{y}={z}{E}{z}\right)\to {x}={y}$
53 52 3expia ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\wedge {z}\in {B}\right)\right)\to \left({x}{E}{y}={z}{E}{z}\to {x}={y}\right)$
54 53 ralrimivvva ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{E}{y}={z}{E}{z}\to {x}={y}\right)$
55 29 54 jca ${⊢}{\phi }\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{E}{y}={y}{E}{x}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{E}{y}={z}{E}{z}\to {x}={y}\right)\right)$
56 4 5 6 istrkgc ${⊢}{H}\in {𝒢}_{\mathrm{Tarski}}^{C}↔\left({H}\in \mathrm{V}\wedge \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{E}{y}={y}{E}{x}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{E}{y}={z}{E}{z}\to {x}={y}\right)\right)\right)$
57 13 55 56 sylanbrc ${⊢}{\phi }\to {H}\in {𝒢}_{\mathrm{Tarski}}^{C}$
58 7 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\to {F}:{B}\underset{1-1 onto}{⟶}{P}$
59 58 30 syl ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\to {F}:{B}\underset{1-1}{⟶}{P}$
60 simp2 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\to \left({x}\in {B}\wedge {y}\in {B}\right)$
61 11 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
62 19 3adant3 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\to {F}\left({x}\right)\in {P}$
63 21 3adant3 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\to {F}\left({y}\right)\in {P}$
64 simp3 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\to {y}\in \left({x}{J}{x}\right)$
65 8 3ad2antl1 ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\right)\right)\to {e}{E}{f}={F}\left({e}\right){D}{F}\left({f}\right)$
66 9 3ad2antl1 ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\right)\to \left({g}\in \left({e}{J}{f}\right)↔{F}\left({g}\right)\in \left({F}\left({e}\right){I}{F}\left({f}\right)\right)\right)$
67 18 3adant3 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\to {x}\in {B}$
68 20 3adant3 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\to {y}\in {B}$
69 1 2 3 4 5 6 58 65 66 67 67 68 f1otrgitv ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\to \left({y}\in \left({x}{J}{x}\right)↔{F}\left({y}\right)\in \left({F}\left({x}\right){I}{F}\left({x}\right)\right)\right)$
70 64 69 mpbid ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\to {F}\left({y}\right)\in \left({F}\left({x}\right){I}{F}\left({x}\right)\right)$
71 1 2 3 61 62 63 70 axtgbtwnid ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\to {F}\left({x}\right)={F}\left({y}\right)$
72 59 60 71 51 syl21anc ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {y}\in \left({x}{J}{x}\right)\right)\to {x}={y}$
73 72 3expia ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({y}\in \left({x}{J}{x}\right)\to {x}={y}\right)$
74 73 ralrimivva ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({x}{J}{x}\right)\to {x}={y}\right)$
75 f1ocnv ${⊢}{F}:{B}\underset{1-1 onto}{⟶}{P}\to {{F}}^{-1}:{P}\underset{1-1 onto}{⟶}{B}$
76 f1of ${⊢}{{F}}^{-1}:{P}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}:{P}⟶{B}$
77 7 75 76 3syl ${⊢}{\phi }\to {{F}}^{-1}:{P}⟶{B}$
78 77 ad5antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {{F}}^{-1}:{P}⟶{B}$
79 simplr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {c}\in {P}$
80 78 79 ffvelrnd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {{F}}^{-1}\left({c}\right)\in {B}$
81 simpr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\wedge {a}={{F}}^{-1}\left({c}\right)\right)\to {a}={{F}}^{-1}\left({c}\right)$
82 81 eleq1d ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\wedge {a}={{F}}^{-1}\left({c}\right)\right)\to \left({a}\in \left({u}{J}{y}\right)↔{{F}}^{-1}\left({c}\right)\in \left({u}{J}{y}\right)\right)$
83 81 eleq1d ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\wedge {a}={{F}}^{-1}\left({c}\right)\right)\to \left({a}\in \left({v}{J}{x}\right)↔{{F}}^{-1}\left({c}\right)\in \left({v}{J}{x}\right)\right)$
84 82 83 anbi12d ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\wedge {a}={{F}}^{-1}\left({c}\right)\right)\to \left(\left({a}\in \left({u}{J}{y}\right)\wedge {a}\in \left({v}{J}{x}\right)\right)↔\left({{F}}^{-1}\left({c}\right)\in \left({u}{J}{y}\right)\wedge {{F}}^{-1}\left({c}\right)\in \left({v}{J}{x}\right)\right)\right)$
85 simprl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)$
86 23 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {F}:{B}\underset{1-1 onto}{⟶}{P}$
87 86 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {F}:{B}\underset{1-1 onto}{⟶}{P}$
88 f1ocnvfv2 ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{P}\wedge {c}\in {P}\right)\to {F}\left({{F}}^{-1}\left({c}\right)\right)={c}$
89 88 eleq1d ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{P}\wedge {c}\in {P}\right)\to \left({F}\left({{F}}^{-1}\left({c}\right)\right)\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)↔{c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\right)$
90 87 79 89 syl2anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to \left({F}\left({{F}}^{-1}\left({c}\right)\right)\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)↔{c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\right)$
91 85 90 mpbird ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {F}\left({{F}}^{-1}\left({c}\right)\right)\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)$
92 24 ad4ant14 ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\right)\right)\to {e}{E}{f}={F}\left({e}\right){D}{F}\left({f}\right)$
93 92 ad4ant14 ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\right)\right)\to {e}{E}{f}={F}\left({e}\right){D}{F}\left({f}\right)$
94 25 ad4ant14 ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\right)\to \left({g}\in \left({e}{J}{f}\right)↔{F}\left({g}\right)\in \left({F}\left({e}\right){I}{F}\left({f}\right)\right)\right)$
95 94 ad4ant14 ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\right)\to \left({g}\in \left({e}{J}{f}\right)↔{F}\left({g}\right)\in \left({F}\left({e}\right){I}{F}\left({f}\right)\right)\right)$
96 simplr2 ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {u}\in {B}$
97 96 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {u}\in {B}$
98 20 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {y}\in {B}$
99 98 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {y}\in {B}$
100 1 2 3 4 5 6 87 93 95 97 99 80 f1otrgitv ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to \left({{F}}^{-1}\left({c}\right)\in \left({u}{J}{y}\right)↔{F}\left({{F}}^{-1}\left({c}\right)\right)\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\right)$
101 91 100 mpbird ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {{F}}^{-1}\left({c}\right)\in \left({u}{J}{y}\right)$
102 simprr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)$
103 88 eleq1d ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{P}\wedge {c}\in {P}\right)\to \left({F}\left({{F}}^{-1}\left({c}\right)\right)\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)↔{c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)$
104 87 79 103 syl2anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to \left({F}\left({{F}}^{-1}\left({c}\right)\right)\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)↔{c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)$
105 102 104 mpbird ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {F}\left({{F}}^{-1}\left({c}\right)\right)\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)$
106 simplr3 ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {v}\in {B}$
107 106 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {v}\in {B}$
108 18 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {x}\in {B}$
109 108 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {x}\in {B}$
110 1 2 3 4 5 6 87 93 95 107 109 80 f1otrgitv ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to \left({{F}}^{-1}\left({c}\right)\in \left({v}{J}{x}\right)↔{F}\left({{F}}^{-1}\left({c}\right)\right)\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)$
111 105 110 mpbird ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to {{F}}^{-1}\left({c}\right)\in \left({v}{J}{x}\right)$
112 101 111 jca ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to \left({{F}}^{-1}\left({c}\right)\in \left({u}{J}{y}\right)\wedge {{F}}^{-1}\left({c}\right)\in \left({v}{J}{x}\right)\right)$
113 80 84 112 rspcedvd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\wedge {c}\in {P}\right)\wedge \left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)\right)\to \exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{J}{y}\right)\wedge {a}\in \left({v}{J}{x}\right)\right)$
114 14 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
115 17 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {F}:{B}⟶{P}$
116 115 108 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {F}\left({x}\right)\in {P}$
117 115 98 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {F}\left({y}\right)\in {P}$
118 simplr1 ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {z}\in {B}$
119 115 118 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {F}\left({z}\right)\in {P}$
120 115 96 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {F}\left({u}\right)\in {P}$
121 115 106 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {F}\left({v}\right)\in {P}$
122 simprl ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {u}\in \left({x}{J}{z}\right)$
123 1 2 3 4 5 6 86 92 94 108 118 96 f1otrgitv ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to \left({u}\in \left({x}{J}{z}\right)↔{F}\left({u}\right)\in \left({F}\left({x}\right){I}{F}\left({z}\right)\right)\right)$
124 122 123 mpbid ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {F}\left({u}\right)\in \left({F}\left({x}\right){I}{F}\left({z}\right)\right)$
125 simprr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {v}\in \left({y}{J}{z}\right)$
126 1 2 3 4 5 6 86 92 94 98 118 106 f1otrgitv ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to \left({v}\in \left({y}{J}{z}\right)↔{F}\left({v}\right)\in \left({F}\left({y}\right){I}{F}\left({z}\right)\right)\right)$
127 125 126 mpbid ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to {F}\left({v}\right)\in \left({F}\left({y}\right){I}{F}\left({z}\right)\right)$
128 1 2 3 114 116 117 119 120 121 124 127 axtgpasch ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to \exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\left({c}\in \left({F}\left({u}\right){I}{F}\left({y}\right)\right)\wedge {c}\in \left({F}\left({v}\right){I}{F}\left({x}\right)\right)\right)$
129 113 128 r19.29a ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\wedge \left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\right)\to \exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{J}{y}\right)\wedge {a}\in \left({v}{J}{x}\right)\right)$
130 129 ex ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({z}\in {B}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\to \left(\left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\to \exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{J}{y}\right)\wedge {a}\in \left({v}{J}{x}\right)\right)\right)$
131 130 ralrimivvva ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {B}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\to \exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{J}{y}\right)\wedge {a}\in \left({v}{J}{x}\right)\right)\right)$
132 131 ralrimivva ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {B}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\to \exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{J}{y}\right)\wedge {a}\in \left({v}{J}{x}\right)\right)\right)$
133 7 ad5antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {F}:{B}\underset{1-1 onto}{⟶}{P}$
134 simpllr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {c}\in {P}$
135 133 134 88 syl2anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {F}\left({{F}}^{-1}\left({c}\right)\right)={c}$
136 ffn ${⊢}{F}:{B}⟶{P}\to {F}Fn{B}$
137 133 15 136 3syl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {F}Fn{B}$
138 simp-4r ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)$
139 138 simpld ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {s}\in 𝒫{B}$
140 139 elpwid ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {s}\subseteq {B}$
141 140 adantlr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {s}\subseteq {B}$
142 simprl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {x}\in {s}$
143 fnfvima ${⊢}\left({F}Fn{B}\wedge {s}\subseteq {B}\wedge {x}\in {s}\right)\to {F}\left({x}\right)\in {F}\left[{s}\right]$
144 137 141 142 143 syl3anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {F}\left({x}\right)\in {F}\left[{s}\right]$
145 138 simprd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {t}\in 𝒫{B}$
146 145 elpwid ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {t}\subseteq {B}$
147 146 adantlr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {t}\subseteq {B}$
148 simprr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {y}\in {t}$
149 fnfvima ${⊢}\left({F}Fn{B}\wedge {t}\subseteq {B}\wedge {y}\in {t}\right)\to {F}\left({y}\right)\in {F}\left[{t}\right]$
150 137 147 148 149 syl3anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {F}\left({y}\right)\in {F}\left[{t}\right]$
151 simplr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)$
152 oveq1 ${⊢}{e}={F}\left({x}\right)\to {e}{I}{f}={F}\left({x}\right){I}{f}$
153 152 eleq2d ${⊢}{e}={F}\left({x}\right)\to \left({c}\in \left({e}{I}{f}\right)↔{c}\in \left({F}\left({x}\right){I}{f}\right)\right)$
154 oveq2 ${⊢}{f}={F}\left({y}\right)\to {F}\left({x}\right){I}{f}={F}\left({x}\right){I}{F}\left({y}\right)$
155 154 eleq2d ${⊢}{f}={F}\left({y}\right)\to \left({c}\in \left({F}\left({x}\right){I}{f}\right)↔{c}\in \left({F}\left({x}\right){I}{F}\left({y}\right)\right)\right)$
156 153 155 rspc2va ${⊢}\left(\left({F}\left({x}\right)\in {F}\left[{s}\right]\wedge {F}\left({y}\right)\in {F}\left[{t}\right]\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\to {c}\in \left({F}\left({x}\right){I}{F}\left({y}\right)\right)$
157 144 150 151 156 syl21anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {c}\in \left({F}\left({x}\right){I}{F}\left({y}\right)\right)$
158 135 157 eqeltrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {F}\left({{F}}^{-1}\left({c}\right)\right)\in \left({F}\left({x}\right){I}{F}\left({y}\right)\right)$
159 7 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {F}:{B}\underset{1-1 onto}{⟶}{P}$
160 simp-5l ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\right)\right)\to {\phi }$
161 160 8 sylancom ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\right)\right)\to {e}{E}{f}={F}\left({e}\right){D}{F}\left({f}\right)$
162 simp-5l ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\right)\to {\phi }$
163 162 9 sylancom ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\right)\to \left({g}\in \left({e}{J}{f}\right)↔{F}\left({g}\right)\in \left({F}\left({e}\right){I}{F}\left({f}\right)\right)\right)$
164 simprl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {x}\in {s}$
165 140 164 sseldd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {x}\in {B}$
166 simprr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {y}\in {t}$
167 146 166 sseldd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {y}\in {B}$
168 77 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {{F}}^{-1}:{P}⟶{B}$
169 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {c}\in {P}$
170 168 169 ffvelrnd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {{F}}^{-1}\left({c}\right)\in {B}$
171 1 2 3 4 5 6 159 161 163 165 167 170 f1otrgitv ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to \left({{F}}^{-1}\left({c}\right)\in \left({x}{J}{y}\right)↔{F}\left({{F}}^{-1}\left({c}\right)\right)\in \left({F}\left({x}\right){I}{F}\left({y}\right)\right)\right)$
172 171 adantlr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to \left({{F}}^{-1}\left({c}\right)\in \left({x}{J}{y}\right)↔{F}\left({{F}}^{-1}\left({c}\right)\right)\in \left({F}\left({x}\right){I}{F}\left({y}\right)\right)\right)$
173 158 172 mpbird ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\wedge \left({x}\in {s}\wedge {y}\in {t}\right)\right)\to {{F}}^{-1}\left({c}\right)\in \left({x}{J}{y}\right)$
174 173 ralrimivva ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\to \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({c}\right)\in \left({x}{J}{y}\right)$
175 174 adantllr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\to \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({c}\right)\in \left({x}{J}{y}\right)$
176 77 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {c}\in {P}\right)\to {{F}}^{-1}:{P}⟶{B}$
177 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {c}\in {P}\right)\to {c}\in {P}$
178 176 177 ffvelrnd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {c}\in {P}\right)\to {{F}}^{-1}\left({c}\right)\in {B}$
179 eleq1 ${⊢}{b}={{F}}^{-1}\left({c}\right)\to \left({b}\in \left({x}{J}{y}\right)↔{{F}}^{-1}\left({c}\right)\in \left({x}{J}{y}\right)\right)$
180 179 2ralbidv ${⊢}{b}={{F}}^{-1}\left({c}\right)\to \left(\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{b}\in \left({x}{J}{y}\right)↔\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({c}\right)\in \left({x}{J}{y}\right)\right)$
181 180 adantl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {c}\in {P}\right)\wedge {b}={{F}}^{-1}\left({c}\right)\right)\to \left(\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{b}\in \left({x}{J}{y}\right)↔\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({c}\right)\in \left({x}{J}{y}\right)\right)$
182 178 181 rspcedv ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {c}\in {P}\right)\to \left(\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({c}\right)\in \left({x}{J}{y}\right)\to \exists {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{b}\in \left({x}{J}{y}\right)\right)$
183 182 adantr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\to \left(\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left({c}\right)\in \left({x}{J}{y}\right)\to \exists {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{b}\in \left({x}{J}{y}\right)\right)$
184 175 183 mpd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {c}\in {P}\right)\wedge \forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)\right)\to \exists {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{b}\in \left({x}{J}{y}\right)$
185 11 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
186 imassrn ${⊢}{F}\left[{s}\right]\subseteq \mathrm{ran}{F}$
187 f1ofo ${⊢}{F}:{B}\underset{1-1 onto}{⟶}{P}\to {F}:{B}\underset{onto}{⟶}{P}$
188 forn ${⊢}{F}:{B}\underset{onto}{⟶}{P}\to \mathrm{ran}{F}={P}$
189 7 187 188 3syl ${⊢}{\phi }\to \mathrm{ran}{F}={P}$
190 189 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\to \mathrm{ran}{F}={P}$
191 186 190 sseqtrid ${⊢}\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\to {F}\left[{s}\right]\subseteq {P}$
192 imassrn ${⊢}{F}\left[{t}\right]\subseteq \mathrm{ran}{F}$
193 192 190 sseqtrid ${⊢}\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\to {F}\left[{t}\right]\subseteq {P}$
194 16 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\to {F}:{B}⟶{P}$
195 simplr ${⊢}\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\to {a}\in {B}$
196 194 195 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\to {F}\left({a}\right)\in {P}$
197 7 ad5antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {F}:{B}\underset{1-1 onto}{⟶}{P}$
198 ffn ${⊢}{{F}}^{-1}:{P}⟶{B}\to {{F}}^{-1}Fn{P}$
199 197 75 76 198 4syl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {{F}}^{-1}Fn{P}$
200 191 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {F}\left[{s}\right]\subseteq {P}$
201 simplr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {u}\in {F}\left[{s}\right]$
202 fnfvima ${⊢}\left({{F}}^{-1}Fn{P}\wedge {F}\left[{s}\right]\subseteq {P}\wedge {u}\in {F}\left[{s}\right]\right)\to {{F}}^{-1}\left({u}\right)\in {{F}}^{-1}\left[{F}\left[{s}\right]\right]$
203 199 200 201 202 syl3anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {{F}}^{-1}\left({u}\right)\in {{F}}^{-1}\left[{F}\left[{s}\right]\right]$
204 197 30 syl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {F}:{B}\underset{1-1}{⟶}{P}$
205 simp-5r ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)$
206 205 simpld ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {s}\in 𝒫{B}$
207 206 elpwid ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {s}\subseteq {B}$
208 f1imacnv ${⊢}\left({F}:{B}\underset{1-1}{⟶}{P}\wedge {s}\subseteq {B}\right)\to {{F}}^{-1}\left[{F}\left[{s}\right]\right]={s}$
209 204 207 208 syl2anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {{F}}^{-1}\left[{F}\left[{s}\right]\right]={s}$
210 203 209 eleqtrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {{F}}^{-1}\left({u}\right)\in {s}$
211 193 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {F}\left[{t}\right]\subseteq {P}$
212 simpr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {v}\in {F}\left[{t}\right]$
213 fnfvima ${⊢}\left({{F}}^{-1}Fn{P}\wedge {F}\left[{t}\right]\subseteq {P}\wedge {v}\in {F}\left[{t}\right]\right)\to {{F}}^{-1}\left({v}\right)\in {{F}}^{-1}\left[{F}\left[{t}\right]\right]$
214 199 211 212 213 syl3anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {{F}}^{-1}\left({v}\right)\in {{F}}^{-1}\left[{F}\left[{t}\right]\right]$
215 205 simprd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {t}\in 𝒫{B}$
216 215 elpwid ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {t}\subseteq {B}$
217 f1imacnv ${⊢}\left({F}:{B}\underset{1-1}{⟶}{P}\wedge {t}\subseteq {B}\right)\to {{F}}^{-1}\left[{F}\left[{t}\right]\right]={t}$
218 204 216 217 syl2anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {{F}}^{-1}\left[{F}\left[{t}\right]\right]={t}$
219 214 218 eleqtrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {{F}}^{-1}\left({v}\right)\in {t}$
220 simpllr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)$
221 eleq1 ${⊢}{x}={{F}}^{-1}\left({u}\right)\to \left({x}\in \left({a}{J}{y}\right)↔{{F}}^{-1}\left({u}\right)\in \left({a}{J}{y}\right)\right)$
222 oveq2 ${⊢}{y}={{F}}^{-1}\left({v}\right)\to {a}{J}{y}={a}{J}{{F}}^{-1}\left({v}\right)$
223 222 eleq2d ${⊢}{y}={{F}}^{-1}\left({v}\right)\to \left({{F}}^{-1}\left({u}\right)\in \left({a}{J}{y}\right)↔{{F}}^{-1}\left({u}\right)\in \left({a}{J}{{F}}^{-1}\left({v}\right)\right)\right)$
224 221 223 rspc2va ${⊢}\left(\left({{F}}^{-1}\left({u}\right)\in {s}\wedge {{F}}^{-1}\left({v}\right)\in {t}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\to {{F}}^{-1}\left({u}\right)\in \left({a}{J}{{F}}^{-1}\left({v}\right)\right)$
225 210 219 220 224 syl21anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {{F}}^{-1}\left({u}\right)\in \left({a}{J}{{F}}^{-1}\left({v}\right)\right)$
226 simp-6l ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\right)\right)\to {\phi }$
227 226 8 sylancom ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\right)\right)\to {e}{E}{f}={F}\left({e}\right){D}{F}\left({f}\right)$
228 simp-6l ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\right)\to {\phi }$
229 228 9 sylancom ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\right)\to \left({g}\in \left({e}{J}{f}\right)↔{F}\left({g}\right)\in \left({F}\left({e}\right){I}{F}\left({f}\right)\right)\right)$
230 simp-4r ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {a}\in {B}$
231 211 212 sseldd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {v}\in {P}$
232 f1ocnvdm ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{P}\wedge {v}\in {P}\right)\to {{F}}^{-1}\left({v}\right)\in {B}$
233 197 231 232 syl2anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {{F}}^{-1}\left({v}\right)\in {B}$
234 200 201 sseldd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {u}\in {P}$
235 f1ocnvdm ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{P}\wedge {u}\in {P}\right)\to {{F}}^{-1}\left({u}\right)\in {B}$
236 197 234 235 syl2anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {{F}}^{-1}\left({u}\right)\in {B}$
237 1 2 3 4 5 6 197 227 229 230 233 236 f1otrgitv ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to \left({{F}}^{-1}\left({u}\right)\in \left({a}{J}{{F}}^{-1}\left({v}\right)\right)↔{F}\left({{F}}^{-1}\left({u}\right)\right)\in \left({F}\left({a}\right){I}{F}\left({{F}}^{-1}\left({v}\right)\right)\right)\right)$
238 225 237 mpbid ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {F}\left({{F}}^{-1}\left({u}\right)\right)\in \left({F}\left({a}\right){I}{F}\left({{F}}^{-1}\left({v}\right)\right)\right)$
239 f1ocnvfv2 ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{P}\wedge {u}\in {P}\right)\to {F}\left({{F}}^{-1}\left({u}\right)\right)={u}$
240 197 234 239 syl2anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {F}\left({{F}}^{-1}\left({u}\right)\right)={u}$
241 f1ocnvfv2 ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{P}\wedge {v}\in {P}\right)\to {F}\left({{F}}^{-1}\left({v}\right)\right)={v}$
242 197 231 241 syl2anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {F}\left({{F}}^{-1}\left({v}\right)\right)={v}$
243 242 oveq2d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {F}\left({a}\right){I}{F}\left({{F}}^{-1}\left({v}\right)\right)={F}\left({a}\right){I}{v}$
244 238 240 243 3eltr3d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\right)\wedge {v}\in {F}\left[{t}\right]\right)\to {u}\in \left({F}\left({a}\right){I}{v}\right)$
245 244 3impa ${⊢}\left(\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\wedge {u}\in {F}\left[{s}\right]\wedge {v}\in {F}\left[{t}\right]\right)\to {u}\in \left({F}\left({a}\right){I}{v}\right)$
246 1 2 3 185 191 193 196 245 axtgcont ${⊢}\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\to \exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\forall {e}\in {F}\left[{s}\right]\phantom{\rule{.4em}{0ex}}\forall {f}\in {F}\left[{t}\right]\phantom{\rule{.4em}{0ex}}{c}\in \left({e}{I}{f}\right)$
247 184 246 r19.29a ${⊢}\left(\left(\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\wedge {a}\in {B}\right)\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\right)\to \exists {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{b}\in \left({x}{J}{y}\right)$
248 247 rexlimdva2 ${⊢}\left({\phi }\wedge \left({s}\in 𝒫{B}\wedge {t}\in 𝒫{B}\right)\right)\to \left(\exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\to \exists {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{b}\in \left({x}{J}{y}\right)\right)$
249 248 ralrimivva ${⊢}{\phi }\to \forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\forall {t}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\left(\exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\to \exists {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{b}\in \left({x}{J}{y}\right)\right)$
250 74 132 249 3jca ${⊢}{\phi }\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({x}{J}{x}\right)\to {x}={y}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {B}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\to \exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{J}{y}\right)\wedge {a}\in \left({v}{J}{x}\right)\right)\right)\wedge \forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\forall {t}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\left(\exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\to \exists {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{b}\in \left({x}{J}{y}\right)\right)\right)$
251 4 5 6 istrkgb ${⊢}{H}\in {𝒢}_{\mathrm{Tarski}}^{B}↔\left({H}\in \mathrm{V}\wedge \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({x}{J}{x}\right)\to {x}={y}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {B}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({x}{J}{z}\right)\wedge {v}\in \left({y}{J}{z}\right)\right)\to \exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{J}{y}\right)\wedge {a}\in \left({v}{J}{x}\right)\right)\right)\wedge \forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\forall {t}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\left(\exists {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{J}{y}\right)\to \exists {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{b}\in \left({x}{J}{y}\right)\right)\right)\right)$
252 13 250 251 sylanbrc ${⊢}{\phi }\to {H}\in {𝒢}_{\mathrm{Tarski}}^{B}$
253 57 252 elind ${⊢}{\phi }\to {H}\in \left({𝒢}_{\mathrm{Tarski}}^{C}\cap {𝒢}_{\mathrm{Tarski}}^{B}\right)$
254 11 ad9antr ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
255 16 ad9antr ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}:{B}⟶{P}$
256 simp-9r ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {x}\in {B}$
257 255 256 ffvelrnd ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({x}\right)\in {P}$
258 simp-8r ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {y}\in {B}$
259 255 258 ffvelrnd ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({y}\right)\in {P}$
260 simp-7r ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {z}\in {B}$
261 255 260 ffvelrnd ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({z}\right)\in {P}$
262 simp-5r ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {a}\in {B}$
263 255 262 ffvelrnd ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({a}\right)\in {P}$
264 simp-4r ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {b}\in {B}$
265 255 264 ffvelrnd ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({b}\right)\in {P}$
266 simpllr ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {c}\in {B}$
267 255 266 ffvelrnd ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({c}\right)\in {P}$
268 simp-6r ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {u}\in {B}$
269 255 268 ffvelrnd ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({u}\right)\in {P}$
270 simplr ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {v}\in {B}$
271 255 270 ffvelrnd ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({v}\right)\in {P}$
272 7 ad9antr ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}:{B}\underset{1-1 onto}{⟶}{P}$
273 272 256 jca ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to \left({F}:{B}\underset{1-1 onto}{⟶}{P}\wedge {x}\in {B}\right)$
274 simprl1 ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {x}\ne {y}$
275 dff1o6 ${⊢}{F}:{B}\underset{1-1 onto}{⟶}{P}↔\left({F}Fn{B}\wedge \mathrm{ran}{F}={P}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)$
276 275 simp3bi ${⊢}{F}:{B}\underset{1-1 onto}{⟶}{P}\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)$
277 276 r19.21bi ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{P}\wedge {x}\in {B}\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)$
278 277 r19.21bi ${⊢}\left(\left({F}:{B}\underset{1-1 onto}{⟶}{P}\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\to \left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)$
279 278 necon3d ${⊢}\left(\left({F}:{B}\underset{1-1 onto}{⟶}{P}\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\to \left({x}\ne {y}\to {F}\left({x}\right)\ne {F}\left({y}\right)\right)$
280 279 imp ${⊢}\left(\left(\left({F}:{B}\underset{1-1 onto}{⟶}{P}\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {x}\ne {y}\right)\to {F}\left({x}\right)\ne {F}\left({y}\right)$
281 273 258 274 280 syl21anc ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({x}\right)\ne {F}\left({y}\right)$
282 simprl2 ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {y}\in \left({x}{J}{z}\right)$
283 8 ex ${⊢}{\phi }\to \left(\left({e}\in {B}\wedge {f}\in {B}\right)\to {e}{E}{f}={F}\left({e}\right){D}{F}\left({f}\right)\right)$
284 283 ad9antr ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to \left(\left({e}\in {B}\wedge {f}\in {B}\right)\to {e}{E}{f}={F}\left({e}\right){D}{F}\left({f}\right)\right)$
285 284 imp ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\right)\right)\to {e}{E}{f}={F}\left({e}\right){D}{F}\left({f}\right)$
286 9 ex ${⊢}{\phi }\to \left(\left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\to \left({g}\in \left({e}{J}{f}\right)↔{F}\left({g}\right)\in \left({F}\left({e}\right){I}{F}\left({f}\right)\right)\right)\right)$
287 286 ad9antr ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to \left(\left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\to \left({g}\in \left({e}{J}{f}\right)↔{F}\left({g}\right)\in \left({F}\left({e}\right){I}{F}\left({f}\right)\right)\right)\right)$
288 287 imp ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\right)\to \left({g}\in \left({e}{J}{f}\right)↔{F}\left({g}\right)\in \left({F}\left({e}\right){I}{F}\left({f}\right)\right)\right)$
289 1 2 3 4 5 6 272 285 288 256 260 258 f1otrgitv ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to \left({y}\in \left({x}{J}{z}\right)↔{F}\left({y}\right)\in \left({F}\left({x}\right){I}{F}\left({z}\right)\right)\right)$
290 282 289 mpbid ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({y}\right)\in \left({F}\left({x}\right){I}{F}\left({z}\right)\right)$
291 simprl3 ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {b}\in \left({a}{J}{c}\right)$
292 1 2 3 4 5 6 272 285 288 262 266 264 f1otrgitv ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to \left({b}\in \left({a}{J}{c}\right)↔{F}\left({b}\right)\in \left({F}\left({a}\right){I}{F}\left({c}\right)\right)\right)$
293 291 292 mpbid ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({b}\right)\in \left({F}\left({a}\right){I}{F}\left({c}\right)\right)$
294 simprr ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)$
295 294 simpld ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to \left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)$
296 295 simpld ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {x}{E}{y}={a}{E}{b}$
297 1 2 3 4 5 6 272 285 288 256 258 f1otrgds ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {x}{E}{y}={F}\left({x}\right){D}{F}\left({y}\right)$
298 1 2 3 4 5 6 272 285 288 262 264 f1otrgds ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {a}{E}{b}={F}\left({a}\right){D}{F}\left({b}\right)$
299 296 297 298 3eqtr3d ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({x}\right){D}{F}\left({y}\right)={F}\left({a}\right){D}{F}\left({b}\right)$
300 295 simprd ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {y}{E}{z}={b}{E}{c}$
301 1 2 3 4 5 6 272 285 288 258 260 f1otrgds ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {y}{E}{z}={F}\left({y}\right){D}{F}\left({z}\right)$
302 1 2 3 4 5 6 272 285 288 264 266 f1otrgds ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {b}{E}{c}={F}\left({b}\right){D}{F}\left({c}\right)$
303 300 301 302 3eqtr3d ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({y}\right){D}{F}\left({z}\right)={F}\left({b}\right){D}{F}\left({c}\right)$
304 294 simprd ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)$
305 304 simpld ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {x}{E}{u}={a}{E}{v}$
306 1 2 3 4 5 6 272 285 288 256 268 f1otrgds ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {x}{E}{u}={F}\left({x}\right){D}{F}\left({u}\right)$
307 1 2 3 4 5 6 272 285 288 262 270 f1otrgds ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {a}{E}{v}={F}\left({a}\right){D}{F}\left({v}\right)$
308 305 306 307 3eqtr3d ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({x}\right){D}{F}\left({u}\right)={F}\left({a}\right){D}{F}\left({v}\right)$
309 304 simprd ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {y}{E}{u}={b}{E}{v}$
310 1 2 3 4 5 6 272 285 288 258 268 f1otrgds ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {y}{E}{u}={F}\left({y}\right){D}{F}\left({u}\right)$
311 1 2 3 4 5 6 272 285 288 264 270 f1otrgds ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {b}{E}{v}={F}\left({b}\right){D}{F}\left({v}\right)$
312 309 310 311 3eqtr3d ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({y}\right){D}{F}\left({u}\right)={F}\left({b}\right){D}{F}\left({v}\right)$
313 1 2 3 254 257 259 261 263 265 267 269 271 281 290 293 299 303 308 312 axtg5seg ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {F}\left({z}\right){D}{F}\left({u}\right)={F}\left({c}\right){D}{F}\left({v}\right)$
314 1 2 3 4 5 6 272 285 288 260 268 f1otrgds ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {z}{E}{u}={F}\left({z}\right){D}{F}\left({u}\right)$
315 1 2 3 4 5 6 272 285 288 266 270 f1otrgds ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {c}{E}{v}={F}\left({c}\right){D}{F}\left({v}\right)$
316 313 314 315 3eqtr4d ${⊢}\left(\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\wedge \left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\right)\to {z}{E}{u}={c}{E}{v}$
317 316 ex ${⊢}\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\wedge {v}\in {B}\right)\to \left(\left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\to {z}{E}{u}={c}{E}{v}\right)$
318 317 ralrimiva ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\wedge {c}\in {B}\right)\to \forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\to {z}{E}{u}={c}{E}{v}\right)$
319 318 ralrimiva ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\to \forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\to {z}{E}{u}={c}{E}{v}\right)$
320 319 ralrimiva ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\wedge {a}\in {B}\right)\to \forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\to {z}{E}{u}={c}{E}{v}\right)$
321 320 ralrimiva ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\wedge {u}\in {B}\right)\to \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\to {z}{E}{u}={c}{E}{v}\right)$
322 321 ralrimiva ${⊢}\left(\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\wedge {z}\in {B}\right)\to \forall {u}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\to {z}{E}{u}={c}{E}{v}\right)$
323 322 ralrimiva ${⊢}\left(\left({\phi }\wedge {x}\in {B}\right)\wedge {y}\in {B}\right)\to \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\to {z}{E}{u}={c}{E}{v}\right)$
324 323 ralrimiva ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\to {z}{E}{u}={c}{E}{v}\right)$
325 324 ralrimiva ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\to {z}{E}{u}={c}{E}{v}\right)$
326 simp-4l ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {\phi }$
327 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {w}\in {P}$
328 simprl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)$
329 326 7 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {F}:{B}\underset{1-1 onto}{⟶}{P}$
330 f1ocnvfv2 ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{P}\wedge {w}\in {P}\right)\to {F}\left({{F}}^{-1}\left({w}\right)\right)={w}$
331 329 327 330 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {F}\left({{F}}^{-1}\left({w}\right)\right)={w}$
332 331 oveq2d ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {F}\left({x}\right){I}{F}\left({{F}}^{-1}\left({w}\right)\right)={F}\left({x}\right){I}{w}$
333 328 332 eleqtrrd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {F}\left({y}\right)\in \left({F}\left({x}\right){I}{F}\left({{F}}^{-1}\left({w}\right)\right)\right)$
334 326 8 sylan ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\right)\right)\to {e}{E}{f}={F}\left({e}\right){D}{F}\left({f}\right)$
335 326 9 sylan ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\wedge \left({e}\in {B}\wedge {f}\in {B}\wedge {g}\in {B}\right)\right)\to \left({g}\in \left({e}{J}{f}\right)↔{F}\left({g}\right)\in \left({F}\left({e}\right){I}{F}\left({f}\right)\right)\right)$
336 18 ad3antrrr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {x}\in {B}$
337 77 ffvelrnda ${⊢}\left({\phi }\wedge {w}\in {P}\right)\to {{F}}^{-1}\left({w}\right)\in {B}$
338 326 327 337 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {{F}}^{-1}\left({w}\right)\in {B}$
339 20 ad3antrrr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {y}\in {B}$
340 1 2 3 4 5 6 329 334 335 336 338 339 f1otrgitv ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to \left({y}\in \left({x}{J}{{F}}^{-1}\left({w}\right)\right)↔{F}\left({y}\right)\in \left({F}\left({x}\right){I}{F}\left({{F}}^{-1}\left({w}\right)\right)\right)\right)$
341 333 340 mpbird ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {y}\in \left({x}{J}{{F}}^{-1}\left({w}\right)\right)$
342 1 2 3 4 5 6 329 334 335 339 338 f1otrgds ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {y}{E}{{F}}^{-1}\left({w}\right)={F}\left({y}\right){D}{F}\left({{F}}^{-1}\left({w}\right)\right)$
343 331 oveq2d ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {F}\left({y}\right){D}{F}\left({{F}}^{-1}\left({w}\right)\right)={F}\left({y}\right){D}{w}$
344 simprr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)$
345 342 343 344 3eqtrd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {y}{E}{{F}}^{-1}\left({w}\right)={F}\left({a}\right){D}{F}\left({b}\right)$
346 simprl ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {a}\in {B}$
347 346 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {a}\in {B}$
348 simprr ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {b}\in {B}$
349 348 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {b}\in {B}$
350 1 2 3 4 5 6 329 334 335 347 349 f1otrgds ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {a}{E}{b}={F}\left({a}\right){D}{F}\left({b}\right)$
351 345 350 eqtr4d ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to {y}{E}{{F}}^{-1}\left({w}\right)={a}{E}{b}$
352 oveq2 ${⊢}{z}={{F}}^{-1}\left({w}\right)\to {x}{J}{z}={x}{J}{{F}}^{-1}\left({w}\right)$
353 352 eleq2d ${⊢}{z}={{F}}^{-1}\left({w}\right)\to \left({y}\in \left({x}{J}{z}\right)↔{y}\in \left({x}{J}{{F}}^{-1}\left({w}\right)\right)\right)$
354 oveq2 ${⊢}{z}={{F}}^{-1}\left({w}\right)\to {y}{E}{z}={y}{E}{{F}}^{-1}\left({w}\right)$
355 354 eqeq1d ${⊢}{z}={{F}}^{-1}\left({w}\right)\to \left({y}{E}{z}={a}{E}{b}↔{y}{E}{{F}}^{-1}\left({w}\right)={a}{E}{b}\right)$
356 353 355 anbi12d ${⊢}{z}={{F}}^{-1}\left({w}\right)\to \left(\left({y}\in \left({x}{J}{z}\right)\wedge {y}{E}{z}={a}{E}{b}\right)↔\left({y}\in \left({x}{J}{{F}}^{-1}\left({w}\right)\right)\wedge {y}{E}{{F}}^{-1}\left({w}\right)={a}{E}{b}\right)\right)$
357 356 adantl ${⊢}\left(\left({\phi }\wedge {w}\in {P}\right)\wedge {z}={{F}}^{-1}\left({w}\right)\right)\to \left(\left({y}\in \left({x}{J}{z}\right)\wedge {y}{E}{z}={a}{E}{b}\right)↔\left({y}\in \left({x}{J}{{F}}^{-1}\left({w}\right)\right)\wedge {y}{E}{{F}}^{-1}\left({w}\right)={a}{E}{b}\right)\right)$
358 337 357 rspcedv ${⊢}\left({\phi }\wedge {w}\in {P}\right)\to \left(\left({y}\in \left({x}{J}{{F}}^{-1}\left({w}\right)\right)\wedge {y}{E}{{F}}^{-1}\left({w}\right)={a}{E}{b}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({x}{J}{z}\right)\wedge {y}{E}{z}={a}{E}{b}\right)\right)$
359 358 imp ${⊢}\left(\left({\phi }\wedge {w}\in {P}\right)\wedge \left({y}\in \left({x}{J}{{F}}^{-1}\left({w}\right)\right)\wedge {y}{E}{{F}}^{-1}\left({w}\right)={a}{E}{b}\right)\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({x}{J}{z}\right)\wedge {y}{E}{z}={a}{E}{b}\right)$
360 326 327 341 351 359 syl22anc ${⊢}\left(\left(\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {w}\in {P}\right)\wedge \left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({x}{J}{z}\right)\wedge {y}{E}{z}={a}{E}{b}\right)$
361 14 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
362 19 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {F}\left({x}\right)\in {P}$
363 21 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {F}\left({y}\right)\in {P}$
364 17 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {F}:{B}⟶{P}$
365 364 346 ffvelrnd ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {F}\left({a}\right)\in {P}$
366 364 348 ffvelrnd ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {F}\left({b}\right)\in {P}$
367 1 2 3 361 362 363 365 366 axtgsegcon ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \exists {w}\in {P}\phantom{\rule{.4em}{0ex}}\left({F}\left({y}\right)\in \left({F}\left({x}\right){I}{w}\right)\wedge {F}\left({y}\right){D}{w}={F}\left({a}\right){D}{F}\left({b}\right)\right)$
368 360 367 r19.29a ${⊢}\left(\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({x}{J}{z}\right)\wedge {y}{E}{z}={a}{E}{b}\right)$
369 368 ralrimivva ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({x}{J}{z}\right)\wedge {y}{E}{z}={a}{E}{b}\right)$
370 369 ralrimivva ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({x}{J}{z}\right)\wedge {y}{E}{z}={a}{E}{b}\right)$
371 13 325 370 jca32 ${⊢}{\phi }\to \left({H}\in \mathrm{V}\wedge \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\to {z}{E}{u}={c}{E}{v}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({x}{J}{z}\right)\wedge {y}{E}{z}={a}{E}{b}\right)\right)\right)$
372 4 5 6 istrkgcb ${⊢}{H}\in {𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}↔\left({H}\in \mathrm{V}\wedge \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\ne {y}\wedge {y}\in \left({x}{J}{z}\right)\wedge {b}\in \left({a}{J}{c}\right)\right)\wedge \left(\left({x}{E}{y}={a}{E}{b}\wedge {y}{E}{z}={b}{E}{c}\right)\wedge \left({x}{E}{u}={a}{E}{v}\wedge {y}{E}{u}={b}{E}{v}\right)\right)\right)\to {z}{E}{u}={c}{E}{v}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({x}{J}{z}\right)\wedge {y}{E}{z}={a}{E}{b}\right)\right)\right)$
373 371 372 sylibr ${⊢}{\phi }\to {H}\in {𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}$
374 4 5 6 istrkgl
375 13 12 374 sylanbrc
376 373 375 elind
377 253 376 elind
378 df-trkg
379 377 378 eleqtrrdi ${⊢}{\phi }\to {H}\in {𝒢}_{\mathrm{Tarski}}$