# Metamath Proof Explorer

## Theorem findcard2d

Description: Deduction version of findcard2 . (Contributed by SO, 16-Jul-2018)

Ref Expression
Hypotheses findcard2d.ch ${⊢}{x}=\varnothing \to \left({\psi }↔{\chi }\right)$
findcard2d.th ${⊢}{x}={y}\to \left({\psi }↔{\theta }\right)$
findcard2d.ta ${⊢}{x}={y}\cup \left\{{z}\right\}\to \left({\psi }↔{\tau }\right)$
findcard2d.et ${⊢}{x}={A}\to \left({\psi }↔{\eta }\right)$
findcard2d.z ${⊢}{\phi }\to {\chi }$
findcard2d.i ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left({\theta }\to {\tau }\right)$
findcard2d.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
Assertion findcard2d ${⊢}{\phi }\to {\eta }$

### Proof

Step Hyp Ref Expression
1 findcard2d.ch ${⊢}{x}=\varnothing \to \left({\psi }↔{\chi }\right)$
2 findcard2d.th ${⊢}{x}={y}\to \left({\psi }↔{\theta }\right)$
3 findcard2d.ta ${⊢}{x}={y}\cup \left\{{z}\right\}\to \left({\psi }↔{\tau }\right)$
4 findcard2d.et ${⊢}{x}={A}\to \left({\psi }↔{\eta }\right)$
5 findcard2d.z ${⊢}{\phi }\to {\chi }$
6 findcard2d.i ${⊢}\left({\phi }\wedge \left({y}\subseteq {A}\wedge {z}\in \left({A}\setminus {y}\right)\right)\right)\to \left({\theta }\to {\tau }\right)$
7 findcard2d.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
8 ssid ${⊢}{A}\subseteq {A}$
9 7 adantr ${⊢}\left({\phi }\wedge {A}\subseteq {A}\right)\to {A}\in \mathrm{Fin}$
10 sseq1 ${⊢}{x}=\varnothing \to \left({x}\subseteq {A}↔\varnothing \subseteq {A}\right)$
11 10 anbi2d ${⊢}{x}=\varnothing \to \left(\left({\phi }\wedge {x}\subseteq {A}\right)↔\left({\phi }\wedge \varnothing \subseteq {A}\right)\right)$
12 11 1 imbi12d ${⊢}{x}=\varnothing \to \left(\left(\left({\phi }\wedge {x}\subseteq {A}\right)\to {\psi }\right)↔\left(\left({\phi }\wedge \varnothing \subseteq {A}\right)\to {\chi }\right)\right)$
13 sseq1 ${⊢}{x}={y}\to \left({x}\subseteq {A}↔{y}\subseteq {A}\right)$
14 13 anbi2d ${⊢}{x}={y}\to \left(\left({\phi }\wedge {x}\subseteq {A}\right)↔\left({\phi }\wedge {y}\subseteq {A}\right)\right)$
15 14 2 imbi12d ${⊢}{x}={y}\to \left(\left(\left({\phi }\wedge {x}\subseteq {A}\right)\to {\psi }\right)↔\left(\left({\phi }\wedge {y}\subseteq {A}\right)\to {\theta }\right)\right)$
16 sseq1 ${⊢}{x}={y}\cup \left\{{z}\right\}\to \left({x}\subseteq {A}↔{y}\cup \left\{{z}\right\}\subseteq {A}\right)$
17 16 anbi2d ${⊢}{x}={y}\cup \left\{{z}\right\}\to \left(\left({\phi }\wedge {x}\subseteq {A}\right)↔\left({\phi }\wedge {y}\cup \left\{{z}\right\}\subseteq {A}\right)\right)$
18 17 3 imbi12d ${⊢}{x}={y}\cup \left\{{z}\right\}\to \left(\left(\left({\phi }\wedge {x}\subseteq {A}\right)\to {\psi }\right)↔\left(\left({\phi }\wedge {y}\cup \left\{{z}\right\}\subseteq {A}\right)\to {\tau }\right)\right)$
19 sseq1 ${⊢}{x}={A}\to \left({x}\subseteq {A}↔{A}\subseteq {A}\right)$
20 19 anbi2d ${⊢}{x}={A}\to \left(\left({\phi }\wedge {x}\subseteq {A}\right)↔\left({\phi }\wedge {A}\subseteq {A}\right)\right)$
21 20 4 imbi12d ${⊢}{x}={A}\to \left(\left(\left({\phi }\wedge {x}\subseteq {A}\right)\to {\psi }\right)↔\left(\left({\phi }\wedge {A}\subseteq {A}\right)\to {\eta }\right)\right)$
22 5 adantr ${⊢}\left({\phi }\wedge \varnothing \subseteq {A}\right)\to {\chi }$
23 simprl ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge ¬{z}\in {y}\right)\wedge \left({\phi }\wedge {y}\cup \left\{{z}\right\}\subseteq {A}\right)\right)\to {\phi }$
24 simprr ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge ¬{z}\in {y}\right)\wedge \left({\phi }\wedge {y}\cup \left\{{z}\right\}\subseteq {A}\right)\right)\to {y}\cup \left\{{z}\right\}\subseteq {A}$
25 24 unssad ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge ¬{z}\in {y}\right)\wedge \left({\phi }\wedge {y}\cup \left\{{z}\right\}\subseteq {A}\right)\right)\to {y}\subseteq {A}$
26 23 25 jca ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge ¬{z}\in {y}\right)\wedge \left({\phi }\wedge {y}\cup \left\{{z}\right\}\subseteq {A}\right)\right)\to \left({\phi }\wedge {y}\subseteq {A}\right)$
27 id ${⊢}{y}\cup \left\{{z}\right\}\subseteq {A}\to {y}\cup \left\{{z}\right\}\subseteq {A}$
28 vsnid ${⊢}{z}\in \left\{{z}\right\}$
29 elun2 ${⊢}{z}\in \left\{{z}\right\}\to {z}\in \left({y}\cup \left\{{z}\right\}\right)$
30 28 29 mp1i ${⊢}{y}\cup \left\{{z}\right\}\subseteq {A}\to {z}\in \left({y}\cup \left\{{z}\right\}\right)$
31 27 30 sseldd ${⊢}{y}\cup \left\{{z}\right\}\subseteq {A}\to {z}\in {A}$
32 31 ad2antll ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge ¬{z}\in {y}\right)\wedge \left({\phi }\wedge {y}\cup \left\{{z}\right\}\subseteq {A}\right)\right)\to {z}\in {A}$
33 simplr ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge ¬{z}\in {y}\right)\wedge \left({\phi }\wedge {y}\cup \left\{{z}\right\}\subseteq {A}\right)\right)\to ¬{z}\in {y}$
34 32 33 eldifd ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge ¬{z}\in {y}\right)\wedge \left({\phi }\wedge {y}\cup \left\{{z}\right\}\subseteq {A}\right)\right)\to {z}\in \left({A}\setminus {y}\right)$
35 23 25 34 6 syl12anc ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge ¬{z}\in {y}\right)\wedge \left({\phi }\wedge {y}\cup \left\{{z}\right\}\subseteq {A}\right)\right)\to \left({\theta }\to {\tau }\right)$
36 26 35 embantd ${⊢}\left(\left({y}\in \mathrm{Fin}\wedge ¬{z}\in {y}\right)\wedge \left({\phi }\wedge {y}\cup \left\{{z}\right\}\subseteq {A}\right)\right)\to \left(\left(\left({\phi }\wedge {y}\subseteq {A}\right)\to {\theta }\right)\to {\tau }\right)$
37 36 ex ${⊢}\left({y}\in \mathrm{Fin}\wedge ¬{z}\in {y}\right)\to \left(\left({\phi }\wedge {y}\cup \left\{{z}\right\}\subseteq {A}\right)\to \left(\left(\left({\phi }\wedge {y}\subseteq {A}\right)\to {\theta }\right)\to {\tau }\right)\right)$
38 37 com23 ${⊢}\left({y}\in \mathrm{Fin}\wedge ¬{z}\in {y}\right)\to \left(\left(\left({\phi }\wedge {y}\subseteq {A}\right)\to {\theta }\right)\to \left(\left({\phi }\wedge {y}\cup \left\{{z}\right\}\subseteq {A}\right)\to {\tau }\right)\right)$
39 12 15 18 21 22 38 findcard2s ${⊢}{A}\in \mathrm{Fin}\to \left(\left({\phi }\wedge {A}\subseteq {A}\right)\to {\eta }\right)$
40 9 39 mpcom ${⊢}\left({\phi }\wedge {A}\subseteq {A}\right)\to {\eta }$
41 8 40 mpan2 ${⊢}{\phi }\to {\eta }$