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		uncom	⊢ ( { 𝑧 } ∪ 𝑦 ) = ( 𝑦 ∪ { 𝑧 } )
9		snssi	⊢ ( 𝑧 ∈ 𝑦 → { 𝑧 } ⊆ 𝑦 )
10		ssequn1	⊢ ( { 𝑧 } ⊆ 𝑦 ↔ ( { 𝑧 } ∪ 𝑦 ) = 𝑦 )
11	9 10	sylib	⊢ ( 𝑧 ∈ 𝑦 → ( { 𝑧 } ∪ 𝑦 ) = 𝑦 )
12	8 11	syl5reqr	⊢ ( 𝑧 ∈ 𝑦 → 𝑦 = ( 𝑦 ∪ { 𝑧 } ) )
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 → 𝜏 )