findcard2d

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

	Ref	Expression
Hypotheses	findcard2d.ch	$⊢ x = \emptyset \to (ψ \leftrightarrow χ)$
	findcard2d.th	$⊢ x = y \to (ψ \leftrightarrow θ)$
	findcard2d.ta	$⊢ x = y \cup \{z\} \to (ψ \leftrightarrow τ)$
	findcard2d.et	$⊢ x = A \to (ψ \leftrightarrow η)$
	findcard2d.z	$⊢ φ \to χ$
	findcard2d.i	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to (θ \to τ)$
	findcard2d.a	$⊢ φ \to A \in Fin$
Assertion	findcard2d	$⊢ φ \to η$

Proof

Step	Hyp	Ref	Expression
1		findcard2d.ch	$⊢ x = \emptyset \to (ψ \leftrightarrow χ)$
2		findcard2d.th	$⊢ x = y \to (ψ \leftrightarrow θ)$
3		findcard2d.ta	$⊢ x = y \cup \{z\} \to (ψ \leftrightarrow τ)$
4		findcard2d.et	$⊢ x = A \to (ψ \leftrightarrow η)$
5		findcard2d.z	$⊢ φ \to χ$
6		findcard2d.i	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to (θ \to τ)$
7		findcard2d.a	$⊢ φ \to A \in Fin$
8		ssid	$⊢ A \subseteq A$
9	7	adantr	$⊢ (φ \land A \subseteq A) \to A \in Fin$
10		sseq1	$⊢ x = \emptyset \to (x \subseteq A \leftrightarrow \emptyset \subseteq A)$
11	10	anbi2d	$⊢ x = \emptyset \to ((φ \land x \subseteq A) \leftrightarrow (φ \land \emptyset \subseteq A))$
12	11 1	imbi12d	$⊢ x = \emptyset \to (((φ \land x \subseteq A) \to ψ) \leftrightarrow ((φ \land \emptyset \subseteq A) \to χ))$
13		sseq1	$⊢ x = y \to (x \subseteq A \leftrightarrow y \subseteq A)$
14	13	anbi2d	$⊢ x = y \to ((φ \land x \subseteq A) \leftrightarrow (φ \land y \subseteq A))$
15	14 2	imbi12d	$⊢ x = y \to (((φ \land x \subseteq A) \to ψ) \leftrightarrow ((φ \land y \subseteq A) \to θ))$
16		sseq1	$⊢ x = y \cup \{z\} \to (x \subseteq A \leftrightarrow y \cup \{z\} \subseteq A)$
17	16	anbi2d	$⊢ x = y \cup \{z\} \to ((φ \land x \subseteq A) \leftrightarrow (φ \land y \cup \{z\} \subseteq A))$
18	17 3	imbi12d	$⊢ x = y \cup \{z\} \to (((φ \land x \subseteq A) \to ψ) \leftrightarrow ((φ \land y \cup \{z\} \subseteq A) \to τ))$
19		sseq1	$⊢ x = A \to (x \subseteq A \leftrightarrow A \subseteq A)$
20	19	anbi2d	$⊢ x = A \to ((φ \land x \subseteq A) \leftrightarrow (φ \land A \subseteq A))$
21	20 4	imbi12d	$⊢ x = A \to (((φ \land x \subseteq A) \to ψ) \leftrightarrow ((φ \land A \subseteq A) \to η))$
22	5	adantr	$⊢ (φ \land \emptyset \subseteq A) \to χ$
23		simprl	$⊢ ((y \in Fin \land \neg z \in y) \land (φ \land y \cup \{z\} \subseteq A)) \to φ$
24		simprr	$⊢ ((y \in Fin \land \neg z \in y) \land (φ \land y \cup \{z\} \subseteq A)) \to y \cup \{z\} \subseteq A$
25	24	unssad	$⊢ ((y \in Fin \land \neg z \in y) \land (φ \land y \cup \{z\} \subseteq A)) \to y \subseteq A$
26	23 25	jca	$⊢ ((y \in Fin \land \neg z \in y) \land (φ \land y \cup \{z\} \subseteq A)) \to (φ \land y \subseteq A)$
27		id	$⊢ y \cup \{z\} \subseteq A \to y \cup \{z\} \subseteq A$
28		vsnid	$⊢ z \in \{z\}$
29		elun2	$⊢ z \in \{z\} \to z \in (y \cup \{z\})$
30	28 29	mp1i	$⊢ y \cup \{z\} \subseteq A \to z \in (y \cup \{z\})$
31	27 30	sseldd	$⊢ y \cup \{z\} \subseteq A \to z \in A$
32	31	ad2antll	$⊢ ((y \in Fin \land \neg z \in y) \land (φ \land y \cup \{z\} \subseteq A)) \to z \in A$
33		simplr	$⊢ ((y \in Fin \land \neg z \in y) \land (φ \land y \cup \{z\} \subseteq A)) \to \neg z \in y$
34	32 33	eldifd	$⊢ ((y \in Fin \land \neg z \in y) \land (φ \land y \cup \{z\} \subseteq A)) \to z \in (A ∖ y)$
35	23 25 34 6	syl12anc	$⊢ ((y \in Fin \land \neg z \in y) \land (φ \land y \cup \{z\} \subseteq A)) \to (θ \to τ)$
36	26 35	embantd	$⊢ ((y \in Fin \land \neg z \in y) \land (φ \land y \cup \{z\} \subseteq A)) \to (((φ \land y \subseteq A) \to θ) \to τ)$
37	36	ex	$⊢ (y \in Fin \land \neg z \in y) \to ((φ \land y \cup \{z\} \subseteq A) \to (((φ \land y \subseteq A) \to θ) \to τ))$
38	37	com23	$⊢ (y \in Fin \land \neg z \in y) \to (((φ \land y \subseteq A) \to θ) \to ((φ \land y \cup \{z\} \subseteq A) \to τ))$
39	12 15 18 21 22 38	findcard2s	$⊢ A \in Fin \to ((φ \land A \subseteq A) \to η)$
40	9 39	mpcom	$⊢ (φ \land A \subseteq A) \to η$
41	8 40	mpan2	$⊢ φ \to η$

Metamath Proof Explorer

Theorem findcard2d

Proof