findcard2s

Description: Variation of findcard2 requiring that the element added in the induction step not be a member of the original set. (Contributed by Paul Chapman, 30-Nov-2012)

	Ref	Expression
Hypotheses	findcard2s.1	$⊢ x = \emptyset \to (φ \leftrightarrow ψ)$
	findcard2s.2	$⊢ x = y \to (φ \leftrightarrow χ)$
	findcard2s.3	$⊢ x = y \cup \{z\} \to (φ \leftrightarrow θ)$
	findcard2s.4	$⊢ x = A \to (φ \leftrightarrow τ)$
	findcard2s.5	$⊢ ψ$
	findcard2s.6	$⊢ (y \in Fin \land \neg z \in y) \to (χ \to θ)$
Assertion	findcard2s	$⊢ A \in Fin \to τ$

Proof

Step	Hyp	Ref	Expression
1		findcard2s.1	$⊢ x = \emptyset \to (φ \leftrightarrow ψ)$
2		findcard2s.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		findcard2s.3	$⊢ x = y \cup \{z\} \to (φ \leftrightarrow θ)$
4		findcard2s.4	$⊢ x = A \to (φ \leftrightarrow τ)$
5		findcard2s.5	$⊢ ψ$
6		findcard2s.6	$⊢ (y \in Fin \land \neg z \in y) \to (χ \to θ)$
7	6	ex	$⊢ y \in Fin \to (\neg z \in y \to (χ \to θ))$
8		snssi	$⊢ z \in y \to \{z\} \subseteq y$
9		ssequn1	$⊢ \{z\} \subseteq y \leftrightarrow \{z\} \cup y = y$
10	8 9	sylib	$⊢ z \in y \to \{z\} \cup y = y$
11		uncom	$⊢ \{z\} \cup y = y \cup \{z\}$
12	10 11	eqtr3di	$⊢ z \in y \to y = y \cup \{z\}$
13		vex	$⊢ y \in V$
14	13	eqvinc	$⊢ y = y \cup \{z\} \leftrightarrow \exists x (x = y \land x = y \cup \{z\})$
15	12 14	sylib	$⊢ z \in y \to \exists x (x = y \land x = y \cup \{z\})$
16	2	bicomd	$⊢ x = y \to (χ \leftrightarrow φ)$
17	16 3	sylan9bb	$⊢ (x = y \land x = y \cup \{z\}) \to (χ \leftrightarrow θ)$
18	17	exlimiv	$⊢ \exists x (x = y \land x = y \cup \{z\}) \to (χ \leftrightarrow θ)$
19	15 18	syl	$⊢ z \in y \to (χ \leftrightarrow θ)$
20	19	biimpd	$⊢ z \in y \to (χ \to θ)$
21	7 20	pm2.61d2	$⊢ y \in Fin \to (χ \to θ)$
22	1 2 3 4 5 21	findcard2	$⊢ A \in Fin \to τ$

Metamath Proof Explorer

Theorem findcard2s

Proof