Theorem findcard2 8611

Description: Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 8-Jul-2010.)

Hypotheses

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

Assertion

Ref	Expression
findcard2	⊢ (𝐴 ∈ Fin → 𝜏)

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

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

Proof of Theorem findcard2

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

Step	Hyp	Ref	Expression
1		findcard2.4	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
2		isfi 8388	. . 3 ⊢ (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥 ≈ 𝑤)
3		breq2 4972	. . . . . . . 8 ⊢ (𝑤 = ∅ → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ ∅))
4	3	imbi1d 343	. . . . . . 7 ⊢ (𝑤 = ∅ → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ ∅ → 𝜑)))
5	4	albidv 1902	. . . . . 6 ⊢ (𝑤 = ∅ → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑)))
6		breq2 4972	. . . . . . . 8 ⊢ (𝑤 = 𝑣 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ 𝑣))
7	6	imbi1d 343	. . . . . . 7 ⊢ (𝑤 = 𝑣 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ 𝑣 → 𝜑)))
8	7	albidv 1902	. . . . . 6 ⊢ (𝑤 = 𝑣 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ 𝑣 → 𝜑)))
9		breq2 4972	. . . . . . . 8 ⊢ (𝑤 = suc 𝑣 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ suc 𝑣))
10	9	imbi1d 343	. . . . . . 7 ⊢ (𝑤 = suc 𝑣 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ suc 𝑣 → 𝜑)))
11	10	albidv 1902	. . . . . 6 ⊢ (𝑤 = suc 𝑣 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑)))
12		en0 8427	. . . . . . . 8 ⊢ (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
13		findcard2.5	. . . . . . . . 9 ⊢ 𝜓
14		findcard2.1	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
15	13, 14	mpbiri 259	. . . . . . . 8 ⊢ (𝑥 = ∅ → 𝜑)
16	12, 15	sylbi 218	. . . . . . 7 ⊢ (𝑥 ≈ ∅ → 𝜑)
17	16	ax-gen 1781	. . . . . 6 ⊢ ∀𝑥(𝑥 ≈ ∅ → 𝜑)
18		nsuceq0 6153	. . . . . . . . . . . 12 ⊢ suc 𝑣 ≠ ∅
19		breq1 4971	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ∅ → (𝑤 ≈ suc 𝑣 ↔ ∅ ≈ suc 𝑣))
20	19	anbi2d 628	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ↔ (𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣)))
21		peano1 7464	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ ω
22		peano2 7465	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ ω → suc 𝑣 ∈ ω)
23		nneneq 8554	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ ω ∧ suc 𝑣 ∈ ω) → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
24	21, 22, 23	sylancr 587	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ ω → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
25	24	biimpa 477	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → ∅ = suc 𝑣)
26	25	eqcomd 2803	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → suc 𝑣 = ∅)
27	20, 26	syl6bi 254	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 = ∅))
28	27	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 = ∅ → suc 𝑣 = ∅))
29	28	necon3d 3007	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (suc 𝑣 ≠ ∅ → 𝑤 ≠ ∅))
30	18, 29	mpi 20	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ≠ ∅)
31	30	ex 413	. . . . . . . . . 10 ⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → 𝑤 ≠ ∅))
32		n0 4236	. . . . . . . . . . . 12 ⊢ (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑤)
33		dif1en 8604	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ∧ 𝑧 ∈ 𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
34	33	3expia 1114	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧 ∈ 𝑤 → (𝑤 ∖ {𝑧}) ≈ 𝑣))
35		snssi 4654	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑤 → {𝑧} ⊆ 𝑤)
36		uncom 4056	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = ({𝑧} ∪ (𝑤 ∖ {𝑧}))
37		undif 4350	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑧} ⊆ 𝑤 ↔ ({𝑧} ∪ (𝑤 ∖ {𝑧})) = 𝑤)
38	37	biimpi 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑧} ⊆ 𝑤 → ({𝑧} ∪ (𝑤 ∖ {𝑧})) = 𝑤)
39	36, 38	syl5eq 2845	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑧} ⊆ 𝑤 → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
40		vex 3443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑤 ∈ V
41	40	difexi 5130	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∖ {𝑧}) ∈ V
42		breq1 4971	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ≈ 𝑣 ↔ (𝑤 ∖ {𝑧}) ≈ 𝑣))
43	42	anbi2d 628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ↔ (𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣)))
44		uneq1 4059	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ∪ {𝑧}) = ((𝑤 ∖ {𝑧}) ∪ {𝑧}))
45	44	sbceq1d 3716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑 ↔ [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
46	45	imbi2d 342	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)))
47	43, 46	imbi12d 346	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) ↔ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))))
48		breq1 4971	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑣 ↔ 𝑦 ≈ 𝑣))
49		findcard2.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
50	48, 49	imbi12d 346	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑣 → 𝜑) ↔ (𝑦 ≈ 𝑣 → 𝜒)))
51	50	spv 2369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → (𝑦 ≈ 𝑣 → 𝜒))
52		rspe 3269	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ∃𝑣 ∈ ω 𝑦 ≈ 𝑣)
53		isfi 8388	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ Fin ↔ ∃𝑣 ∈ ω 𝑦 ≈ 𝑣)
54	52, 53	sylibr 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → 𝑦 ∈ Fin)
55		pm2.27 42	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ≈ 𝑣 → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒))
56	55	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒))
57		findcard2.6	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃))
58	54, 56, 57	sylsyld 61	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜃))
59	51, 58	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → 𝜃))
60		vex 3443	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑦 ∈ V
61		snex 5230	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑧} ∈ V
62	60, 61	unex 7333	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∪ {𝑧}) ∈ V
63		findcard2.3	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))
64	62, 63	sbcie 3746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑 ↔ 𝜃)
65	59, 64	syl6ibr 253	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑))
66	41, 47, 65	vtocl 3505	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
67		dfsbcq 3713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ([((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑 ↔ [𝑤 / 𝑥]𝜑))
68	67	imbi2d 342	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
69	66, 68	syl5ib 245	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
70	35, 39, 69	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
71	70	expd 416	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑤 → (𝑣 ∈ ω → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
72	71	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ω → (𝑧 ∈ 𝑤 → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
73	72	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧 ∈ 𝑤 → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
74	34, 73	mpdd 43	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧 ∈ 𝑤 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
75	74	exlimdv 1915	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∃𝑧 𝑧 ∈ 𝑤 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
76	32, 75	syl5bi 243	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
77	76	ex 413	. . . . . . . . . 10 ⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (𝑤 ≠ ∅ → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
78	31, 77	mpdd 43	. . . . . . . . 9 ⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
79	78	com23 86	. . . . . . . 8 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → (𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
80	79	alrimdv 1911	. . . . . . 7 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → ∀𝑤(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
81		nfv 1896	. . . . . . . 8 ⊢ Ⅎ𝑤(𝑥 ≈ suc 𝑣 → 𝜑)
82		nfv 1896	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑤 ≈ suc 𝑣
83		nfsbc1v 3731	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝜑
84	82, 83	nfim 1882	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)
85		breq1 4971	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑥 ≈ suc 𝑣 ↔ 𝑤 ≈ suc 𝑣))
86		sbceq1a 3722	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑))
87	85, 86	imbi12d 346	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ((𝑥 ≈ suc 𝑣 → 𝜑) ↔ (𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
88	81, 84, 87	cbvalv1 2322	. . . . . . 7 ⊢ (∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑) ↔ ∀𝑤(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑))
89	80, 88	syl6ibr 253	. . . . . 6 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑)))
90	5, 8, 11, 17, 89	finds1 7474	. . . . 5 ⊢ (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑))
91	90	19.21bi 2154	. . . 4 ⊢ (𝑤 ∈ ω → (𝑥 ≈ 𝑤 → 𝜑))
92	91	rexlimiv 3245	. . 3 ⊢ (∃𝑤 ∈ ω 𝑥 ≈ 𝑤 → 𝜑)
93	2, 92	sylbi 218	. 2 ⊢ (𝑥 ∈ Fin → 𝜑)
94	1, 93	vtoclga 3519	1 ⊢ (𝐴 ∈ Fin → 𝜏)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1523   = wceq 1525  ∃wex 1765   ∈ wcel 2083   ≠ wne 2986  ∃wrex 3108  [wsbc 3711   ∖ cdif 3862   ∪ cun 3863   ⊆ wss 3865  ∅c0 4217  {csn 4478   class class class wbr 4968  suc csuc 6075  ωcom 7443   ≈ cen 8361  Fincfn 8364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-om 7444  df-1o 7960  df-er 8146  df-en 8365  df-fin 8368

This theorem is referenced by:  findcard2s  8612  frfi  8616  fnfi  8649  iunfi  8665  finsschain  8684  infdiffi  8974  fin1a2lem10  9684  wunfi  9996  rexfiuz  14545  modfsummod  14986  lcmfunsnlem  15818  lcmfun  15822  drsdirfi  17381  fiuncmp  21700  finiunmbl  23832  mbfresfi  34490  heibor1lem  34640  pclfinclN  36638