# Metamath Proof Explorer

## Theorem kmlem2

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004)

Ref Expression
Assertion kmlem2 ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(¬{y}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 ineq2 ${⊢}{y}={v}\to {z}\cap {y}={z}\cap {v}$
2 1 eleq2d ${⊢}{y}={v}\to \left({w}\in \left({z}\cap {y}\right)↔{w}\in \left({z}\cap {v}\right)\right)$
3 2 eubidv ${⊢}{y}={v}\to \left(\exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)↔\exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {v}\right)\right)$
4 3 imbi2d ${⊢}{y}={v}\to \left(\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)↔\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {v}\right)\right)\right)$
5 4 ralbidv ${⊢}{y}={v}\to \left(\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)↔\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {v}\right)\right)\right)$
6 5 cbvexvw ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)↔\exists {v}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {v}\right)\right)$
7 indi ${⊢}{z}\cap \left({v}\cup \left\{{u}\right\}\right)=\left({z}\cap {v}\right)\cup \left({z}\cap \left\{{u}\right\}\right)$
8 elssuni ${⊢}{z}\in {x}\to {z}\subseteq \bigcup {x}$
9 8 ssneld ${⊢}{z}\in {x}\to \left(¬{u}\in \bigcup {x}\to ¬{u}\in {z}\right)$
10 disjsn ${⊢}{z}\cap \left\{{u}\right\}=\varnothing ↔¬{u}\in {z}$
11 9 10 syl6ibr ${⊢}{z}\in {x}\to \left(¬{u}\in \bigcup {x}\to {z}\cap \left\{{u}\right\}=\varnothing \right)$
12 11 impcom ${⊢}\left(¬{u}\in \bigcup {x}\wedge {z}\in {x}\right)\to {z}\cap \left\{{u}\right\}=\varnothing$
13 12 uneq2d ${⊢}\left(¬{u}\in \bigcup {x}\wedge {z}\in {x}\right)\to \left({z}\cap {v}\right)\cup \left({z}\cap \left\{{u}\right\}\right)=\left({z}\cap {v}\right)\cup \varnothing$
14 un0 ${⊢}\left({z}\cap {v}\right)\cup \varnothing ={z}\cap {v}$
15 13 14 syl6eq ${⊢}\left(¬{u}\in \bigcup {x}\wedge {z}\in {x}\right)\to \left({z}\cap {v}\right)\cup \left({z}\cap \left\{{u}\right\}\right)={z}\cap {v}$
16 7 15 syl5req ${⊢}\left(¬{u}\in \bigcup {x}\wedge {z}\in {x}\right)\to {z}\cap {v}={z}\cap \left({v}\cup \left\{{u}\right\}\right)$
17 16 eleq2d ${⊢}\left(¬{u}\in \bigcup {x}\wedge {z}\in {x}\right)\to \left({w}\in \left({z}\cap {v}\right)↔{w}\in \left({z}\cap \left({v}\cup \left\{{u}\right\}\right)\right)\right)$
18 17 eubidv ${⊢}\left(¬{u}\in \bigcup {x}\wedge {z}\in {x}\right)\to \left(\exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {v}\right)↔\exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap \left({v}\cup \left\{{u}\right\}\right)\right)\right)$
19 18 imbi2d ${⊢}\left(¬{u}\in \bigcup {x}\wedge {z}\in {x}\right)\to \left(\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {v}\right)\right)↔\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap \left({v}\cup \left\{{u}\right\}\right)\right)\right)\right)$
20 19 ralbidva ${⊢}¬{u}\in \bigcup {x}\to \left(\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {v}\right)\right)↔\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap \left({v}\cup \left\{{u}\right\}\right)\right)\right)\right)$
21 vsnid ${⊢}{u}\in \left\{{u}\right\}$
22 21 olci ${⊢}\left({u}\in {v}\vee {u}\in \left\{{u}\right\}\right)$
23 elun ${⊢}{u}\in \left({v}\cup \left\{{u}\right\}\right)↔\left({u}\in {v}\vee {u}\in \left\{{u}\right\}\right)$
24 22 23 mpbir ${⊢}{u}\in \left({v}\cup \left\{{u}\right\}\right)$
25 elssuni ${⊢}{v}\cup \left\{{u}\right\}\in {x}\to {v}\cup \left\{{u}\right\}\subseteq \bigcup {x}$
26 25 sseld ${⊢}{v}\cup \left\{{u}\right\}\in {x}\to \left({u}\in \left({v}\cup \left\{{u}\right\}\right)\to {u}\in \bigcup {x}\right)$
27 24 26 mpi ${⊢}{v}\cup \left\{{u}\right\}\in {x}\to {u}\in \bigcup {x}$
28 27 con3i ${⊢}¬{u}\in \bigcup {x}\to ¬{v}\cup \left\{{u}\right\}\in {x}$
29 28 biantrurd ${⊢}¬{u}\in \bigcup {x}\to \left(\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap \left({v}\cup \left\{{u}\right\}\right)\right)\right)↔\left(¬{v}\cup \left\{{u}\right\}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap \left({v}\cup \left\{{u}\right\}\right)\right)\right)\right)\right)$
30 20 29 bitrd ${⊢}¬{u}\in \bigcup {x}\to \left(\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {v}\right)\right)↔\left(¬{v}\cup \left\{{u}\right\}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap \left({v}\cup \left\{{u}\right\}\right)\right)\right)\right)\right)$
31 vex ${⊢}{v}\in \mathrm{V}$
32 snex ${⊢}\left\{{u}\right\}\in \mathrm{V}$
33 31 32 unex ${⊢}{v}\cup \left\{{u}\right\}\in \mathrm{V}$
34 eleq1 ${⊢}{y}={v}\cup \left\{{u}\right\}\to \left({y}\in {x}↔{v}\cup \left\{{u}\right\}\in {x}\right)$
35 34 notbid ${⊢}{y}={v}\cup \left\{{u}\right\}\to \left(¬{y}\in {x}↔¬{v}\cup \left\{{u}\right\}\in {x}\right)$
36 ineq2 ${⊢}{y}={v}\cup \left\{{u}\right\}\to {z}\cap {y}={z}\cap \left({v}\cup \left\{{u}\right\}\right)$
37 36 eleq2d ${⊢}{y}={v}\cup \left\{{u}\right\}\to \left({w}\in \left({z}\cap {y}\right)↔{w}\in \left({z}\cap \left({v}\cup \left\{{u}\right\}\right)\right)\right)$
38 37 eubidv ${⊢}{y}={v}\cup \left\{{u}\right\}\to \left(\exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)↔\exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap \left({v}\cup \left\{{u}\right\}\right)\right)\right)$
39 38 imbi2d ${⊢}{y}={v}\cup \left\{{u}\right\}\to \left(\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)↔\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap \left({v}\cup \left\{{u}\right\}\right)\right)\right)\right)$
40 39 ralbidv ${⊢}{y}={v}\cup \left\{{u}\right\}\to \left(\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)↔\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap \left({v}\cup \left\{{u}\right\}\right)\right)\right)\right)$
41 35 40 anbi12d ${⊢}{y}={v}\cup \left\{{u}\right\}\to \left(\left(¬{y}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)\right)↔\left(¬{v}\cup \left\{{u}\right\}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap \left({v}\cup \left\{{u}\right\}\right)\right)\right)\right)\right)$
42 33 41 spcev ${⊢}\left(¬{v}\cup \left\{{u}\right\}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap \left({v}\cup \left\{{u}\right\}\right)\right)\right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left(¬{y}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)\right)$
43 30 42 syl6bi ${⊢}¬{u}\in \bigcup {x}\to \left(\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {v}\right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left(¬{y}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)\right)\right)$
44 vuniex ${⊢}\bigcup {x}\in \mathrm{V}$
45 eleq2 ${⊢}{y}=\bigcup {x}\to \left({u}\in {y}↔{u}\in \bigcup {x}\right)$
46 45 notbid ${⊢}{y}=\bigcup {x}\to \left(¬{u}\in {y}↔¬{u}\in \bigcup {x}\right)$
47 46 exbidv ${⊢}{y}=\bigcup {x}\to \left(\exists {u}\phantom{\rule{.4em}{0ex}}¬{u}\in {y}↔\exists {u}\phantom{\rule{.4em}{0ex}}¬{u}\in \bigcup {x}\right)$
48 nalset ${⊢}¬\exists {y}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}{u}\in {y}$
49 alexn ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}¬{u}\in {y}↔¬\exists {y}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}{u}\in {y}$
50 48 49 mpbir ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}¬{u}\in {y}$
51 50 spi ${⊢}\exists {u}\phantom{\rule{.4em}{0ex}}¬{u}\in {y}$
52 44 47 51 vtocl ${⊢}\exists {u}\phantom{\rule{.4em}{0ex}}¬{u}\in \bigcup {x}$
53 43 52 exlimiiv ${⊢}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {v}\right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left(¬{y}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)\right)$
54 53 exlimiv ${⊢}\exists {v}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {v}\right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left(¬{y}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)\right)$
55 6 54 sylbi ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left(¬{y}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)\right)$
56 exsimpr ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left(¬{y}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)$
57 55 56 impbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(¬{y}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists !{w}\phantom{\rule{.4em}{0ex}}{w}\in \left({z}\cap {y}\right)\right)\right)$