# Metamath Proof Explorer

Description: An entry of the adjunct (cofactor) matrix. (Contributed by SO, 17-Jul-2018)

Ref Expression
Hypotheses madufval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
madufval.d ${⊢}{D}={N}\mathrm{maDet}{R}$
madufval.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
madufval.b ${⊢}{B}={\mathrm{Base}}_{{A}}$

### Proof

Step Hyp Ref Expression
1 madufval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 madufval.d ${⊢}{D}={N}\mathrm{maDet}{R}$
3 madufval.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
4 madufval.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
7 eleq2 ${⊢}{m}=\varnothing \to \left({k}\in {m}↔{k}\in \varnothing \right)$
8 7 ifbid
9 8 ifeq2d
10 9 mpoeq3dv
11 10 fveq2d
12 11 eqeq2d
13 eleq2 ${⊢}{m}={n}\to \left({k}\in {m}↔{k}\in {n}\right)$
14 13 ifbid
15 14 ifeq2d
16 15 mpoeq3dv
17 16 fveq2d
18 17 eqeq2d
19 eleq2 ${⊢}{m}={n}\cup \left\{{r}\right\}\to \left({k}\in {m}↔{k}\in \left({n}\cup \left\{{r}\right\}\right)\right)$
20 19 ifbid
21 20 ifeq2d
22 21 mpoeq3dv
23 22 fveq2d
24 23 eqeq2d
25 eleq2 ${⊢}{m}={N}\setminus \left\{{H}\right\}\to \left({k}\in {m}↔{k}\in \left({N}\setminus \left\{{H}\right\}\right)\right)$
26 25 ifbid
27 26 ifeq2d
28 27 mpoeq3dv
29 28 fveq2d
30 29 eqeq2d
31 1 2 3 4 5 6 maducoeval
33 noel ${⊢}¬{k}\in \varnothing$
34 iffalse
35 33 34 mp1i
36 35 ifeq2d
37 36 mpoeq3ia
38 37 fveq2i
39 32 38 syl6eqr
40 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
41 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
42 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
43 simpl1l ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\to {R}\in \mathrm{CRing}$
44 simp1r ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\to {M}\in {B}$
45 1 4 matrcl ${⊢}{M}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
46 45 simpld ${⊢}{M}\in {B}\to {N}\in \mathrm{Fin}$
47 44 46 syl ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\to {N}\in \mathrm{Fin}$
48 47 adantr ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\to {N}\in \mathrm{Fin}$
49 simp1l ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\to {R}\in \mathrm{CRing}$
50 49 ad2antrr ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {l}\in {N}\right)\to {R}\in \mathrm{CRing}$
51 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
52 50 51 syl ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {l}\in {N}\right)\to {R}\in \mathrm{Ring}$
53 40 6 ring0cl
54 52 53 syl
55 simpl1r ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\to {M}\in {B}$
56 1 40 4 matbas2i ${⊢}{M}\in {B}\to {M}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
57 elmapi ${⊢}{M}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
58 55 56 57 3syl ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
59 58 adantr ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {l}\in {N}\right)\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
60 eldifi ${⊢}{r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\to {r}\in \left({N}\setminus \left\{{H}\right\}\right)$
61 60 ad2antll ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\to {r}\in \left({N}\setminus \left\{{H}\right\}\right)$
62 61 eldifad ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\to {r}\in {N}$
63 62 adantr ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {l}\in {N}\right)\to {r}\in {N}$
64 simpr ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {l}\in {N}\right)\to {l}\in {N}$
65 59 63 64 fovrnd ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {l}\in {N}\right)\to {r}{M}{l}\in {\mathrm{Base}}_{{R}}$
66 54 65 ifcld
67 40 5 ringidcl
68 52 67 syl
69 68 54 ifcld
71 58 fovrnda ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge \left({k}\in {N}\wedge {l}\in {N}\right)\right)\to {k}{M}{l}\in {\mathrm{Base}}_{{R}}$
72 71 3impb ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to {k}{M}{l}\in {\mathrm{Base}}_{{R}}$
73 70 72 ifcld
74 73 72 ifcld
75 simpl2 ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\to {I}\in {N}$
76 58 62 75 fovrnd ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\to {r}{M}{I}\in {\mathrm{Base}}_{{R}}$
77 simpl3 ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\to {H}\in {N}$
78 eldifsni ${⊢}{r}\in \left({N}\setminus \left\{{H}\right\}\right)\to {r}\ne {H}$
79 61 78 syl ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\to {r}\ne {H}$
80 2 40 41 42 43 48 66 69 74 76 62 77 79 mdetero
81 ifnot
82 81 eqcomi
83 82 a1i
84 ovif2
85 76 adantr ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {l}\in {N}\right)\to {r}{M}{I}\in {\mathrm{Base}}_{{R}}$
86 40 42 5 ringridm
87 52 85 86 syl2anc
89 oveq2 ${⊢}{l}={I}\to {r}{M}{l}={r}{M}{I}$
90 89 adantl ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {l}\in {N}\right)\wedge {l}={I}\right)\to {r}{M}{l}={r}{M}{I}$
91 88 90 eqtr4d
92 91 ifeq1da
93 40 42 6 ringrz
94 52 85 93 syl2anc
95 94 ifeq2d
96 92 95 eqtrd
97 84 96 syl5eq
98 83 97 oveq12d
99 ringmnd ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Mnd}$
100 52 99 syl ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {l}\in {N}\right)\to {R}\in \mathrm{Mnd}$
101 id ${⊢}¬{l}={I}\to ¬{l}={I}$
102 imnan ${⊢}\left(¬{l}={I}\to ¬{l}={I}\right)↔¬\left(¬{l}={I}\wedge {l}={I}\right)$
103 101 102 mpbi ${⊢}¬\left(¬{l}={I}\wedge {l}={I}\right)$
104 103 a1i ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {l}\in {N}\right)\to ¬\left(¬{l}={I}\wedge {l}={I}\right)$
105 40 6 41 mndifsplit
106 100 65 104 105 syl3anc
107 pm2.1 ${⊢}\left(¬{l}={I}\vee {l}={I}\right)$
108 iftrue
109 107 108 mp1i
110 98 106 109 3eqtr2d
112 oveq1 ${⊢}{k}={r}\to {k}{M}{l}={r}{M}{l}$
113 112 eqeq2d
114 111 113 syl5ibrcom
115 114 imp
116 iftrue
118 79 neneqd ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\to ¬{r}={H}$
119 118 3ad2ant1 ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to ¬{r}={H}$
120 eqeq1 ${⊢}{k}={r}\to \left({k}={H}↔{r}={H}\right)$
121 120 notbid ${⊢}{k}={r}\to \left(¬{k}={H}↔¬{r}={H}\right)$
122 119 121 syl5ibrcom ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to \left({k}={r}\to ¬{k}={H}\right)$
123 122 imp ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\wedge {k}={r}\right)\to ¬{k}={H}$
124 123 iffalsed
125 eldifn ${⊢}{r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\to ¬{r}\in {n}$
126 125 ad2antll ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\to ¬{r}\in {n}$
127 126 3ad2ant1 ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to ¬{r}\in {n}$
128 eleq1w ${⊢}{k}={r}\to \left({k}\in {n}↔{r}\in {n}\right)$
129 128 notbid ${⊢}{k}={r}\to \left(¬{k}\in {n}↔¬{r}\in {n}\right)$
130 127 129 syl5ibrcom ${⊢}\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to \left({k}={r}\to ¬{k}\in {n}\right)$
131 130 imp ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\wedge \left({n}\subseteq {N}\setminus \left\{{H}\right\}\wedge {r}\in \left(\left({N}\setminus \left\{{H}\right\}\right)\setminus {n}\right)\right)\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\wedge {k}={r}\right)\to ¬{k}\in {n}$
132 131 iffalsed
133 124 132 eqtrd
134 115 117 133 3eqtr4d
135 iffalse
137 134 136 pm2.61dan
138 137 mpoeq3dva
139 138 fveq2d
140 neeq2 ${⊢}{k}={H}\to \left({r}\ne {k}↔{r}\ne {H}\right)$
141 140 biimparc ${⊢}\left({r}\ne {H}\wedge {k}={H}\right)\to {r}\ne {k}$
142 141 necomd ${⊢}\left({r}\ne {H}\wedge {k}={H}\right)\to {k}\ne {r}$
143 142 neneqd ${⊢}\left({r}\ne {H}\wedge {k}={H}\right)\to ¬{k}={r}$
144 143 iffalsed
145 iftrue
147 146 ifeq2d
148 iftrue
150 144 147 149 3eqtr4d
151 112 ifeq2d
152 vsnid ${⊢}{r}\in \left\{{r}\right\}$
153 elun2 ${⊢}{r}\in \left\{{r}\right\}\to {r}\in \left({n}\cup \left\{{r}\right\}\right)$
154 152 153 ax-mp ${⊢}{r}\in \left({n}\cup \left\{{r}\right\}\right)$
155 eleq1w ${⊢}{k}={r}\to \left({k}\in \left({n}\cup \left\{{r}\right\}\right)↔{r}\in \left({n}\cup \left\{{r}\right\}\right)\right)$
156 154 155 mpbiri ${⊢}{k}={r}\to {k}\in \left({n}\cup \left\{{r}\right\}\right)$
157 156 iftrued
158 iftrue
159 151 157 158 3eqtr4rd
161 iffalse
162 orc ${⊢}{k}\in {n}\to \left({k}\in {n}\vee {k}={r}\right)$
163 orel2 ${⊢}¬{k}={r}\to \left(\left({k}\in {n}\vee {k}={r}\right)\to {k}\in {n}\right)$
164 162 163 impbid2 ${⊢}¬{k}={r}\to \left({k}\in {n}↔\left({k}\in {n}\vee {k}={r}\right)\right)$
165 elun ${⊢}{k}\in \left({n}\cup \left\{{r}\right\}\right)↔\left({k}\in {n}\vee {k}\in \left\{{r}\right\}\right)$
166 velsn ${⊢}{k}\in \left\{{r}\right\}↔{k}={r}$
167 166 orbi2i ${⊢}\left({k}\in {n}\vee {k}\in \left\{{r}\right\}\right)↔\left({k}\in {n}\vee {k}={r}\right)$
168 165 167 bitr2i ${⊢}\left({k}\in {n}\vee {k}={r}\right)↔{k}\in \left({n}\cup \left\{{r}\right\}\right)$
169 164 168 syl6bb ${⊢}¬{k}={r}\to \left({k}\in {n}↔{k}\in \left({n}\cup \left\{{r}\right\}\right)\right)$
170 169 ifbid
171 161 170 eqtrd
173 160 172 pm2.61dan
174 iffalse
175 174 ifeq2d
177 iffalse
179 173 176 178 3eqtr4d
180 150 179 pm2.61dan
181 180 mpoeq3dv
182 181 fveq2d
183 79 182 syl
184 80 139 183 3eqtr3d
185 184 eqeq2d
186 185 biimpd
187 difss ${⊢}{N}\setminus \left\{{H}\right\}\subseteq {N}$
188 ssfi ${⊢}\left({N}\in \mathrm{Fin}\wedge {N}\setminus \left\{{H}\right\}\subseteq {N}\right)\to {N}\setminus \left\{{H}\right\}\in \mathrm{Fin}$
189 47 187 188 sylancl ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {I}\in {N}\wedge {H}\in {N}\right)\to {N}\setminus \left\{{H}\right\}\in \mathrm{Fin}$
190 12 18 24 30 39 186 189 findcard2d
191 iba ${⊢}{k}={H}\to \left({l}={I}↔\left({l}={I}\wedge {k}={H}\right)\right)$
192 191 ifbid
193 iftrue
194 iftrue
195 194 orcs
196 192 193 195 3eqtr4d
198 iffalse
200 neqne ${⊢}¬{k}={H}\to {k}\ne {H}$
201 200 anim2i ${⊢}\left({k}\in {N}\wedge ¬{k}={H}\right)\to \left({k}\in {N}\wedge {k}\ne {H}\right)$
202 201 adantlr ${⊢}\left(\left({k}\in {N}\wedge {l}\in {N}\right)\wedge ¬{k}={H}\right)\to \left({k}\in {N}\wedge {k}\ne {H}\right)$
203 eldifsn ${⊢}{k}\in \left({N}\setminus \left\{{H}\right\}\right)↔\left({k}\in {N}\wedge {k}\ne {H}\right)$
204 202 203 sylibr ${⊢}\left(\left({k}\in {N}\wedge {l}\in {N}\right)\wedge ¬{k}={H}\right)\to {k}\in \left({N}\setminus \left\{{H}\right\}\right)$
205 204 iftrued
206 biorf ${⊢}¬{k}={H}\to \left({l}={I}↔\left({k}={H}\vee {l}={I}\right)\right)$
207 id ${⊢}¬{k}={H}\to ¬{k}={H}$
208 207 intnand ${⊢}¬{k}={H}\to ¬\left({l}={I}\wedge {k}={H}\right)$
209 208 iffalsed
210 209 eqcomd
211 206 210 ifbieq1d