Theorem findcard2s 6777

Description: Variation of findcard2 6776 requiring that the element added in the induction step not be a member of the original set. (Contributed by Paul Chapman, 30-Nov-2012.)

Hypotheses

Ref	Expression
findcard2s.1	⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
findcard2s.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
findcard2s.3	⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))
findcard2s.4	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
findcard2s.5	⊢ 𝜓
findcard2s.6	⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝜒 → 𝜃))

Assertion

Ref	Expression
findcard2s	⊢ (𝐴 ∈ Fin → 𝜏)

Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝜒,𝑥   𝜑,𝑦,𝑧   𝜓,𝑥   𝜏,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦,𝑧)   𝜒(𝑦,𝑧)   𝜃(𝑦,𝑧)   𝜏(𝑦,𝑧)

Proof of Theorem findcard2s

Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		findcard2s.4	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
2		isfi 6648	. . 3 ⊢ (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥 ≈ 𝑤)
3		breq2 3928	. . . . . . . 8 ⊢ (𝑤 = ∅ → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ ∅))
4	3	imbi1d 230	. . . . . . 7 ⊢ (𝑤 = ∅ → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ ∅ → 𝜑)))
5	4	albidv 1796	. . . . . 6 ⊢ (𝑤 = ∅ → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑)))
6		breq2 3928	. . . . . . . 8 ⊢ (𝑤 = 𝑣 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ 𝑣))
7	6	imbi1d 230	. . . . . . 7 ⊢ (𝑤 = 𝑣 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ 𝑣 → 𝜑)))
8	7	albidv 1796	. . . . . 6 ⊢ (𝑤 = 𝑣 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ 𝑣 → 𝜑)))
9		breq2 3928	. . . . . . . 8 ⊢ (𝑤 = suc 𝑣 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ suc 𝑣))
10	9	imbi1d 230	. . . . . . 7 ⊢ (𝑤 = suc 𝑣 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ suc 𝑣 → 𝜑)))
11	10	albidv 1796	. . . . . 6 ⊢ (𝑤 = suc 𝑣 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑)))
12		en0 6682	. . . . . . . 8 ⊢ (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
13		findcard2s.5	. . . . . . . . 9 ⊢ 𝜓
14		findcard2s.1	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
15	13, 14	mpbiri 167	. . . . . . . 8 ⊢ (𝑥 = ∅ → 𝜑)
16	12, 15	sylbi 120	. . . . . . 7 ⊢ (𝑥 ≈ ∅ → 𝜑)
17	16	ax-gen 1425	. . . . . 6 ⊢ ∀𝑥(𝑥 ≈ ∅ → 𝜑)
18		peano3 4505	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ω → suc 𝑣 ≠ ∅)
19	18	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ≠ ∅)
20		breq1 3927	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ∅ → (𝑤 ≈ suc 𝑣 ↔ ∅ ≈ suc 𝑣))
21	20	anbi2d 459	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ↔ (𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣)))
22		peano1 4503	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ ω
23		peano2 4504	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ ω → suc 𝑣 ∈ ω)
24		nneneq 6744	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ ω ∧ suc 𝑣 ∈ ω) → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
25	22, 23, 24	sylancr 410	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ ω → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
26	25	biimpa 294	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → ∅ = suc 𝑣)
27	26	eqcomd 2143	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → suc 𝑣 = ∅)
28	21, 27	syl6bi 162	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 = ∅))
29	28	com12 30	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 = ∅ → suc 𝑣 = ∅))
30	29	necon3d 2350	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (suc 𝑣 ≠ ∅ → 𝑤 ≠ ∅))
31	19, 30	mpd 13	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ≠ ∅)
32	31	ex 114	. . . . . . . . . 10 ⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → 𝑤 ≠ ∅))
33		nnfi 6759	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑣 ∈ ω → suc 𝑣 ∈ Fin)
34	23, 33	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ω → suc 𝑣 ∈ Fin)
35	34	adantr 274	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 ∈ Fin)
36		enfi 6760	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ≈ suc 𝑣 → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin))
37	36	adantl 275	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ∈ Fin ↔ suc 𝑣 ∈ Fin))
38	35, 37	mpbird 166	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ∈ Fin)
39		fin0 6772	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ Fin → (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑤))
40	38, 39	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑤))
41		simpll 518	. . . . . . . . . . . . . . 15 ⊢ (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧 ∈ 𝑤) → 𝑣 ∈ ω)
42		dif1en 6766	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ∧ 𝑧 ∈ 𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
43	42	3expa 1181	. . . . . . . . . . . . . . 15 ⊢ (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧 ∈ 𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
44		fidifsnid 6758	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ Fin ∧ 𝑧 ∈ 𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
45	38, 44	sylan 281	. . . . . . . . . . . . . . . 16 ⊢ (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧 ∈ 𝑤) → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
46		neldifsn 3648	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})
47		vex 2684	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑤 ∈ V
48		difexg 4064	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ V → (𝑤 ∖ {𝑧}) ∈ V)
49	47, 48	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∖ {𝑧}) ∈ V
50		breq1 3927	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ≈ 𝑣 ↔ (𝑤 ∖ {𝑧}) ≈ 𝑣))
51	50	anbi2d 459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ↔ (𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣)))
52		eleq2 2201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ (𝑤 ∖ {𝑧})))
53	52	notbid 656	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (¬ 𝑧 ∈ 𝑦 ↔ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})))
54	51, 53	anbi12d 464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) ↔ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧}))))
55		uneq1 3218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ∪ {𝑧}) = ((𝑤 ∖ {𝑧}) ∪ {𝑧}))
56	55	sbceq1d 2909	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑 ↔ [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
57	56	imbi2d 229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)))
58	54, 57	imbi12d 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) ↔ (((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))))
59		breq1 3927	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑣 ↔ 𝑦 ≈ 𝑣))
60		findcard2s.2	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
61	59, 60	imbi12d 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑣 → 𝜑) ↔ (𝑦 ≈ 𝑣 → 𝜒)))
62	61	spv 1832	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → (𝑦 ≈ 𝑣 → 𝜒))
63		pm2.27 40	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ≈ 𝑣 → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒))
64	63	adantl 275	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒))
65	64	adantr 274	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒))
66		rspe 2479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ∃𝑣 ∈ ω 𝑦 ≈ 𝑣)
67		isfi 6648	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ Fin ↔ ∃𝑣 ∈ ω 𝑦 ≈ 𝑣)
68	66, 67	sylibr 133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → 𝑦 ∈ Fin)
69		findcard2s.6	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝜒 → 𝜃))
70	68, 69	sylan 281	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) → (𝜒 → 𝜃))
71	65, 70	syld 45	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜃))
72	62, 71	syl5 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → 𝜃))
73		vex 2684	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑦 ∈ V
74		vex 2684	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
75	74	snex 4104	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑧} ∈ V
76	73, 75	unex 4357	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∪ {𝑧}) ∈ V
77		findcard2s.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))
78	76, 77	sbcie 2938	. . . . . . . . . . . . . . . . . . . 20 ⊢ ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑 ↔ 𝜃)
79	72, 78	syl6ibr 161	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑))
80	49, 58, 79	vtocl 2735	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) ∧ ¬ 𝑧 ∈ (𝑤 ∖ {𝑧})) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
81	46, 80	mpan2 421	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
82		dfsbcq 2906	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ([((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑 ↔ [𝑤 / 𝑥]𝜑))
83	82	imbi2d 229	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
84	81, 83	syl5ib 153	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
85	45, 84	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧 ∈ 𝑤) → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
86	41, 43, 85	mp2and 429	. . . . . . . . . . . . . 14 ⊢ (((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ∧ 𝑧 ∈ 𝑤) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))
87	86	ex 114	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧 ∈ 𝑤 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
88	87	exlimdv 1791	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∃𝑧 𝑧 ∈ 𝑤 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
89	40, 88	sylbid 149	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
90	89	ex 114	. . . . . . . . . 10 ⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (𝑤 ≠ ∅ → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
91	32, 90	mpdd 41	. . . . . . . . 9 ⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
92	91	com23 78	. . . . . . . 8 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → (𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
93	92	alrimdv 1848	. . . . . . 7 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → ∀𝑤(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
94		nfv 1508	. . . . . . . 8 ⊢ Ⅎ𝑤(𝑥 ≈ suc 𝑣 → 𝜑)
95		nfv 1508	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑤 ≈ suc 𝑣
96		nfsbc1v 2922	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝜑
97	95, 96	nfim 1551	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)
98		breq1 3927	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑥 ≈ suc 𝑣 ↔ 𝑤 ≈ suc 𝑣))
99		sbceq1a 2913	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑))
100	98, 99	imbi12d 233	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ((𝑥 ≈ suc 𝑣 → 𝜑) ↔ (𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
101	94, 97, 100	cbval 1727	. . . . . . 7 ⊢ (∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑) ↔ ∀𝑤(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑))
102	93, 101	syl6ibr 161	. . . . . 6 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑)))
103	5, 8, 11, 17, 102	finds1 4511	. . . . 5 ⊢ (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑))
104	103	19.21bi 1537	. . . 4 ⊢ (𝑤 ∈ ω → (𝑥 ≈ 𝑤 → 𝜑))
105	104	rexlimiv 2541	. . 3 ⊢ (∃𝑤 ∈ ω 𝑥 ≈ 𝑤 → 𝜑)
106	2, 105	sylbi 120	. 2 ⊢ (𝑥 ∈ Fin → 𝜑)
107	1, 106	vtoclga 2747	1 ⊢ (𝐴 ∈ Fin → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1329   = wceq 1331  ∃wex 1468   ∈ wcel 1480   ≠ wne 2306  ∃wrex 2415  Vcvv 2681  [wsbc 2904   ∖ cdif 3063   ∪ cun 3064  ∅c0 3358  {csn 3522   class class class wbr 3924  suc csuc 4282  ωcom 4499   ≈ cen 6625  Fincfn 6627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-coll 4038  ax-sep 4041  ax-nul 4049  ax-pow 4093  ax-pr 4126  ax-un 4350  ax-setind 4447  ax-iinf 4497

This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-ral 2419  df-rex 2420  df-reu 2421  df-rab 2423  df-v 2683  df-sbc 2905  df-csb 2999  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-nul 3359  df-if 3470  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-int 3767  df-iun 3810  df-br 3925  df-opab 3985  df-mpt 3986  df-tr 4022  df-id 4210  df-iord 4283  df-on 4285  df-suc 4288  df-iom 4500  df-xp 4540  df-rel 4541  df-cnv 4542  df-co 4543  df-dm 4544  df-rn 4545  df-res 4546  df-ima 4547  df-iota 5083  df-fun 5120  df-fn 5121  df-f 5122  df-f1 5123  df-fo 5124  df-f1o 5125  df-fv 5126  df-er 6422  df-en 6628  df-fin 6630

This theorem is referenced by:  findcard2d  6778  findcard2sd  6779  diffifi  6781  ac6sfi  6785  fisseneq  6813  fsum2d  11197  modfsummod  11220  fsumabs  11227  fsumiun  11239