# Metamath Proof Explorer

## Theorem cdlemk36

Description: Part of proof of Lemma K of Crawley p. 118. TODO: fix comment. (Contributed by NM, 18-Jul-2013)

Ref Expression
Hypotheses cdlemk4.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdlemk4.l
cdlemk4.j
cdlemk4.m
cdlemk4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemk4.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemk4.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemk4.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemk4.z
cdlemk4.y
cdlemk4.x ${⊢}{X}=\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {z}\left({P}\right)={Y}\right)\right)$
Assertion cdlemk36

### Proof

Step Hyp Ref Expression
1 cdlemk4.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemk4.l
3 cdlemk4.j
4 cdlemk4.m
5 cdlemk4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 cdlemk4.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 cdlemk4.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
8 cdlemk4.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
9 cdlemk4.z
10 cdlemk4.y
11 cdlemk4.x ${⊢}{X}=\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {z}\left({P}\right)={Y}\right)\right)$
12 11 eqcomi ${⊢}\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {z}\left({P}\right)={Y}\right)\right)={X}$
13 simpl1
14 simpl2
15 simpl3
16 simpr1
17 simpr2
18 simpr3
19 1 2 3 4 5 6 7 8 9 10 11 cdlemk35
20 13 14 15 16 17 18 19 syl132anc
21 11 20 eqeltrrid
22 7 fvexi ${⊢}{T}\in \mathrm{V}$
23 22 riotaclbBAD ${⊢}\exists !{z}\in {T}\phantom{\rule{.4em}{0ex}}\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {z}\left({P}\right)={Y}\right)↔\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {z}\left({P}\right)={Y}\right)\right)\in {T}$
24 21 23 sylibr
25 nfriota1 ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {z}\left({P}\right)={Y}\right)\right)$
26 11 25 nfcxfr ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{X}$
27 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{T}$
28 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)$
29 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{P}$
30 26 29 nffv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{X}\left({P}\right)$
31 30 nfeq1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{X}\left({P}\right)={Y}$
32 28 31 nfim ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {X}\left({P}\right)={Y}\right)$
33 27 32 nfralw ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {X}\left({P}\right)={Y}\right)$
34 nfra1 ${⊢}Ⅎ{b}\phantom{\rule{.4em}{0ex}}\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {z}\left({P}\right)={Y}\right)$
35 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{T}$
36 34 35 nfriota ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {z}\left({P}\right)={Y}\right)\right)$
37 11 36 nfcxfr ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{X}$
38 37 nfeq2 ${⊢}Ⅎ{b}\phantom{\rule{.4em}{0ex}}{z}={X}$
39 fveq1 ${⊢}{z}={X}\to {z}\left({P}\right)={X}\left({P}\right)$
40 39 eqeq1d ${⊢}{z}={X}\to \left({z}\left({P}\right)={Y}↔{X}\left({P}\right)={Y}\right)$
41 40 imbi2d ${⊢}{z}={X}\to \left(\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {z}\left({P}\right)={Y}\right)↔\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {X}\left({P}\right)={Y}\right)\right)$
42 38 41 ralbid ${⊢}{z}={X}\to \left(\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {z}\left({P}\right)={Y}\right)↔\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {X}\left({P}\right)={Y}\right)\right)$
43 26 33 42 riota2f ${⊢}\left({X}\in {T}\wedge \exists !{z}\in {T}\phantom{\rule{.4em}{0ex}}\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {z}\left({P}\right)={Y}\right)\right)\to \left(\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {X}\left({P}\right)={Y}\right)↔\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {z}\left({P}\right)={Y}\right)\right)={X}\right)$
44 20 24 43 syl2anc
45 12 44 mpbiri
46 rsp ${⊢}\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {X}\left({P}\right)={Y}\right)\to \left({b}\in {T}\to \left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({G}\right)\right)\to {X}\left({P}\right)={Y}\right)\right)$
47 45 46 syl
48 47 impd
49 48 3impia