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 ( 𝑥 = ∅ → ( 𝜑𝜓 ) )
findcard2s.2 ( 𝑥 = 𝑦 → ( 𝜑𝜒 ) )
findcard2s.3 ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝜑𝜃 ) )
findcard2s.4 ( 𝑥 = 𝐴 → ( 𝜑𝜏 ) )
findcard2s.5 𝜓
findcard2s.6 ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) → ( 𝜒𝜃 ) )
Assertion findcard2s ( 𝐴 ∈ Fin → 𝜏 )

Proof

Step Hyp Ref Expression
1 findcard2s.1 ( 𝑥 = ∅ → ( 𝜑𝜓 ) )
2 findcard2s.2 ( 𝑥 = 𝑦 → ( 𝜑𝜒 ) )
3 findcard2s.3 ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝜑𝜃 ) )
4 findcard2s.4 ( 𝑥 = 𝐴 → ( 𝜑𝜏 ) )
5 findcard2s.5 𝜓
6 findcard2s.6 ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) → ( 𝜒𝜃 ) )
7 6 ex ( 𝑦 ∈ Fin → ( ¬ 𝑧𝑦 → ( 𝜒𝜃 ) ) )
8 snssi ( 𝑧𝑦 → { 𝑧 } ⊆ 𝑦 )
9 ssequn1 ( { 𝑧 } ⊆ 𝑦 ↔ ( { 𝑧 } ∪ 𝑦 ) = 𝑦 )
10 8 9 sylib ( 𝑧𝑦 → ( { 𝑧 } ∪ 𝑦 ) = 𝑦 )
11 uncom ( { 𝑧 } ∪ 𝑦 ) = ( 𝑦 ∪ { 𝑧 } )
12 10 11 eqtr3di ( 𝑧𝑦𝑦 = ( 𝑦 ∪ { 𝑧 } ) )
13 vex 𝑦 ∈ V
14 13 eqvinc ( 𝑦 = ( 𝑦 ∪ { 𝑧 } ) ↔ ∃ 𝑥 ( 𝑥 = 𝑦𝑥 = ( 𝑦 ∪ { 𝑧 } ) ) )
15 12 14 sylib ( 𝑧𝑦 → ∃ 𝑥 ( 𝑥 = 𝑦𝑥 = ( 𝑦 ∪ { 𝑧 } ) ) )
16 2 bicomd ( 𝑥 = 𝑦 → ( 𝜒𝜑 ) )
17 16 3 sylan9bb ( ( 𝑥 = 𝑦𝑥 = ( 𝑦 ∪ { 𝑧 } ) ) → ( 𝜒𝜃 ) )
18 17 exlimiv ( ∃ 𝑥 ( 𝑥 = 𝑦𝑥 = ( 𝑦 ∪ { 𝑧 } ) ) → ( 𝜒𝜃 ) )
19 15 18 syl ( 𝑧𝑦 → ( 𝜒𝜃 ) )
20 19 biimpd ( 𝑧𝑦 → ( 𝜒𝜃 ) )
21 7 20 pm2.61d2 ( 𝑦 ∈ Fin → ( 𝜒𝜃 ) )
22 1 2 3 4 5 21 findcard2 ( 𝐴 ∈ Fin → 𝜏 )