Metamath Proof Explorer

Theorem 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 = ∅ → φ ↔ ψ
findcard2s.2 ⊢ x = y → φ ↔ χ
findcard2s.3 ⊢ x = y ∪ z → φ ↔ θ
findcard2s.4 ⊢ x = A → φ ↔ τ
findcard2s.5 ⊢ ψ
findcard2s.6 ⊢ y ∈ Fin ∧ ¬ z ∈ y → χ → θ
Assertion findcard2s ⊢ A ∈ Fin → τ

Proof

Step Hyp Ref Expression
1 findcard2s.1 ⊢ x = ∅ → φ ↔ ψ
2 findcard2s.2 ⊢ x = y → φ ↔ χ
3 findcard2s.3 ⊢ x = y ∪ z → φ ↔ θ
4 findcard2s.4 ⊢ x = A → φ ↔ τ
5 findcard2s.5 ⊢ ψ
6 findcard2s.6 ⊢ y ∈ Fin ∧ ¬ z ∈ y → χ → θ
7 6 ex ⊢ y ∈ Fin → ¬ z ∈ y → χ → θ
8 uncom ⊢ z ∪ y = y ∪ z
9 snssi ⊢ z ∈ y → z ⊆ y
10 ssequn1 ⊢ z ⊆ y ↔ z ∪ y = y
11 9 10 sylib ⊢ z ∈ y → z ∪ y = y
12 8 11 syl5reqr ⊢ z ∈ y → y = y ∪ z
13 vex ⊢ y ∈ V
14 13 eqvinc ⊢ y = y ∪ z ↔ ∃ x x = y ∧ x = y ∪ z
15 12 14 sylib ⊢ z ∈ y → ∃ x x = y ∧ x = y ∪ z
16 2 bicomd ⊢ x = y → χ ↔ φ
17 16 3 sylan9bb ⊢ x = y ∧ x = y ∪ z → χ ↔ θ
18 17 exlimiv ⊢ ∃ x x = y ∧ x = y ∪ z → χ ↔ θ
19 15 18 syl ⊢ z ∈ y → χ ↔ θ
20 19 biimpd ⊢ z ∈ y → χ → θ
21 7 20 pm2.61d2 ⊢ y ∈ Fin → χ → θ
22 1 2 3 4 5 21 findcard2 ⊢ A ∈ Fin → τ