This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 → 𝜏 )