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 snssi z y z y
9 ssequn1 z y z y = y
10 8 9 sylib z y z y = y
11 uncom z y = y z
12 10 11 eqtr3di 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 τ