# Metamath Proof Explorer

## Theorem bnj1174

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1174.3 ${⊢}{C}=trCl\left({X},{A},{R}\right)\cap {B}$
bnj1174.59 ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\right)\right)$
bnj1174.74 ${⊢}{\theta }\to \left({w}{R}{z}\to {w}\in trCl\left({X},{A},{R}\right)\right)$
Assertion bnj1174 ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left(\left({\phi }\wedge {\psi }\wedge {z}\in {C}\right)\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 bnj1174.3 ${⊢}{C}=trCl\left({X},{A},{R}\right)\cap {B}$
2 bnj1174.59 ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\right)\right)$
3 bnj1174.74 ${⊢}{\theta }\to \left({w}{R}{z}\to {w}\in trCl\left({X},{A},{R}\right)\right)$
4 1 eleq2i ${⊢}{w}\in {C}↔{w}\in \left(trCl\left({X},{A},{R}\right)\cap {B}\right)$
5 4 notbii ${⊢}¬{w}\in {C}↔¬{w}\in \left(trCl\left({X},{A},{R}\right)\cap {B}\right)$
6 ianor ${⊢}¬\left({w}\in trCl\left({X},{A},{R}\right)\wedge {w}\in {B}\right)↔\left(¬{w}\in trCl\left({X},{A},{R}\right)\vee ¬{w}\in {B}\right)$
7 elin ${⊢}{w}\in \left(trCl\left({X},{A},{R}\right)\cap {B}\right)↔\left({w}\in trCl\left({X},{A},{R}\right)\wedge {w}\in {B}\right)$
8 7 notbii ${⊢}¬{w}\in \left(trCl\left({X},{A},{R}\right)\cap {B}\right)↔¬\left({w}\in trCl\left({X},{A},{R}\right)\wedge {w}\in {B}\right)$
9 pm4.62 ${⊢}\left({w}\in trCl\left({X},{A},{R}\right)\to ¬{w}\in {B}\right)↔\left(¬{w}\in trCl\left({X},{A},{R}\right)\vee ¬{w}\in {B}\right)$
10 6 8 9 3bitr4i ${⊢}¬{w}\in \left(trCl\left({X},{A},{R}\right)\cap {B}\right)↔\left({w}\in trCl\left({X},{A},{R}\right)\to ¬{w}\in {B}\right)$
11 10 biimpi ${⊢}¬{w}\in \left(trCl\left({X},{A},{R}\right)\cap {B}\right)\to \left({w}\in trCl\left({X},{A},{R}\right)\to ¬{w}\in {B}\right)$
12 11 impcom ${⊢}\left({w}\in trCl\left({X},{A},{R}\right)\wedge ¬{w}\in \left(trCl\left({X},{A},{R}\right)\cap {B}\right)\right)\to ¬{w}\in {B}$
13 5 12 sylan2b ${⊢}\left({w}\in trCl\left({X},{A},{R}\right)\wedge ¬{w}\in {C}\right)\to ¬{w}\in {B}$
14 13 ex ${⊢}{w}\in trCl\left({X},{A},{R}\right)\to \left(¬{w}\in {C}\to ¬{w}\in {B}\right)$
15 3 14 syl6 ${⊢}{\theta }\to \left({w}{R}{z}\to \left(¬{w}\in {C}\to ¬{w}\in {B}\right)\right)$
16 15 a2d ${⊢}{\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)$
17 16 biantru ${⊢}\left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\right)↔\left(\left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$
18 df-3an ${⊢}\left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)↔\left(\left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$
19 3anass ${⊢}\left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)↔\left({z}\in {C}\wedge \left(\left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\right)$
20 17 18 19 3bitr2i ${⊢}\left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\right)↔\left({z}\in {C}\wedge \left(\left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\right)$
21 20 imbi2i ${⊢}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\right)\right)↔\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left(\left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\right)\right)$
22 21 albii ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\right)\right)↔\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left(\left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\right)\right)$
23 22 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left(\left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\right)\right)$
24 2 23 mpbi ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left(\left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\right)\right)$
25 imdi ${⊢}\left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)↔\left(\left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\to \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)$
26 pm3.35 ${⊢}\left(\left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\wedge \left(\left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\to \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\to \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)$
27 25 26 sylan2b ${⊢}\left(\left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\to \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)$
28 27 anim2i ${⊢}\left({z}\in {C}\wedge \left(\left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\right)\to \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)$
29 28 imim2i ${⊢}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left(\left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\right)\right)\to \left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$
30 29 alimi ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left(\left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {C}\right)\right)\wedge \left({\theta }\to \left(\left({w}{R}{z}\to ¬{w}\in {C}\right)\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\right)\right)\to \forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$
31 24 30 bnj101 ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$
32 ancl ${⊢}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\to \left(\left({\phi }\wedge {\psi }\right)\to \left(\left({\phi }\wedge {\psi }\right)\wedge \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\right)$
33 bnj256 ${⊢}\left({\phi }\wedge {\psi }\wedge {z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)↔\left(\left({\phi }\wedge {\psi }\right)\wedge \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$
34 32 33 syl6ibr ${⊢}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\to \left(\left({\phi }\wedge {\psi }\right)\to \left({\phi }\wedge {\psi }\wedge {z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$
35 34 alimi ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)\to \forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({\phi }\wedge {\psi }\wedge {z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$
36 31 35 bnj101 ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({\phi }\wedge {\psi }\wedge {z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$
37 df-bnj17 ${⊢}\left({\phi }\wedge {\psi }\wedge {z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)↔\left(\left({\phi }\wedge {\psi }\wedge {z}\in {C}\right)\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)$
38 37 imbi2i ${⊢}\left(\left({\phi }\wedge {\psi }\right)\to \left({\phi }\wedge {\psi }\wedge {z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)↔\left(\left({\phi }\wedge {\psi }\right)\to \left(\left({\phi }\wedge {\psi }\wedge {z}\in {C}\right)\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$
39 38 albii ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({\phi }\wedge {\psi }\wedge {z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)↔\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left(\left({\phi }\wedge {\psi }\wedge {z}\in {C}\right)\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$
40 39 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left({\phi }\wedge {\psi }\wedge {z}\in {C}\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left(\left({\phi }\wedge {\psi }\wedge {z}\in {C}\right)\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$
41 36 40 mpbi ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to \left(\left({\phi }\wedge {\psi }\wedge {z}\in {C}\right)\wedge \left({\theta }\to \left({w}{R}{z}\to ¬{w}\in {B}\right)\right)\right)\right)$