Theorem findcard2OLD 9311

Description: Obsolete version of findcard2 9194 as of 6-Aug-2024. (Contributed by Jeff Madsen, 8-Jul-2010.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

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

Assertion

Ref	Expression
findcard2OLD	⊢ (𝐴 ∈ Fin → 𝜏)

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

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

Proof of Theorem findcard2OLD

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

Step	Hyp	Ref	Expression
1		findcard2OLD.4	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
2		isfi 8999	. . 3 ⊢ (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥 ≈ 𝑤)
3		breq2 5149	. . . . . . . 8 ⊢ (𝑤 = ∅ → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ ∅))
4	3	imbi1d 340	. . . . . . 7 ⊢ (𝑤 = ∅ → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ ∅ → 𝜑)))
5	4	albidv 1916	. . . . . 6 ⊢ (𝑤 = ∅ → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑)))
6		breq2 5149	. . . . . . . 8 ⊢ (𝑤 = 𝑣 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ 𝑣))
7	6	imbi1d 340	. . . . . . 7 ⊢ (𝑤 = 𝑣 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ 𝑣 → 𝜑)))
8	7	albidv 1916	. . . . . 6 ⊢ (𝑤 = 𝑣 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ 𝑣 → 𝜑)))
9		breq2 5149	. . . . . . . 8 ⊢ (𝑤 = suc 𝑣 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ suc 𝑣))
10	9	imbi1d 340	. . . . . . 7 ⊢ (𝑤 = suc 𝑣 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ suc 𝑣 → 𝜑)))
11	10	albidv 1916	. . . . . 6 ⊢ (𝑤 = suc 𝑣 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑)))
12		en0 9041	. . . . . . . 8 ⊢ (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
13		findcard2OLD.5	. . . . . . . . 9 ⊢ 𝜓
14		findcard2OLD.1	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
15	13, 14	mpbiri 257	. . . . . . . 8 ⊢ (𝑥 = ∅ → 𝜑)
16	12, 15	sylbi 216	. . . . . . 7 ⊢ (𝑥 ≈ ∅ → 𝜑)
17	16	ax-gen 1790	. . . . . 6 ⊢ ∀𝑥(𝑥 ≈ ∅ → 𝜑)
18		nsuceq0 6451	. . . . . . . . . . . 12 ⊢ suc 𝑣 ≠ ∅
19		breq1 5148	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ∅ → (𝑤 ≈ suc 𝑣 ↔ ∅ ≈ suc 𝑣))
20	19	anbi2d 628	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ↔ (𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣)))
21		peano1 7892	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ ω
22		peano2 7894	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ ω → suc 𝑣 ∈ ω)
23		nneneq 9236	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ ω ∧ suc 𝑣 ∈ ω) → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
24	21, 22, 23	sylancr 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ ω → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
25	24	biimpa 475	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → ∅ = suc 𝑣)
26	25	eqcomd 2732	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → suc 𝑣 = ∅)
27	20, 26	biimtrdi 252	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 = ∅))
28	27	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 = ∅ → suc 𝑣 = ∅))
29	28	necon3d 2951	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (suc 𝑣 ≠ ∅ → 𝑤 ≠ ∅))
30	18, 29	mpi 20	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ≠ ∅)
31	30	ex 411	. . . . . . . . . 10 ⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → 𝑤 ≠ ∅))
32		n0 4346	. . . . . . . . . . . 12 ⊢ (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑤)
33		dif1enOLD 9192	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ∧ 𝑧 ∈ 𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
34	33	3expia 1118	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧 ∈ 𝑤 → (𝑤 ∖ {𝑧}) ≈ 𝑣))
35		snssi 4807	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑤 → {𝑧} ⊆ 𝑤)
36		uncom 4150	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = ({𝑧} ∪ (𝑤 ∖ {𝑧}))
37		undif 4476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑧} ⊆ 𝑤 ↔ ({𝑧} ∪ (𝑤 ∖ {𝑧})) = 𝑤)
38	37	biimpi 215	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑧} ⊆ 𝑤 → ({𝑧} ∪ (𝑤 ∖ {𝑧})) = 𝑤)
39	36, 38	eqtrid 2778	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑧} ⊆ 𝑤 → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
40		vex 3466	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑤 ∈ V
41	40	difexi 5327	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∖ {𝑧}) ∈ V
42		breq1 5148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ≈ 𝑣 ↔ (𝑤 ∖ {𝑧}) ≈ 𝑣))
43	42	anbi2d 628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ↔ (𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣)))
44		uneq1 4153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ∪ {𝑧}) = ((𝑤 ∖ {𝑧}) ∪ {𝑧}))
45	44	sbceq1d 3780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑 ↔ [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
46	45	imbi2d 339	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)))
47	43, 46	imbi12d 343	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) ↔ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))))
48		breq1 5148	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑣 ↔ 𝑦 ≈ 𝑣))
49		findcard2OLD.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
50	48, 49	imbi12d 343	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑣 → 𝜑) ↔ (𝑦 ≈ 𝑣 → 𝜒)))
51	50	spvv 1993	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → (𝑦 ≈ 𝑣 → 𝜒))
52		rspe 3237	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ∃𝑣 ∈ ω 𝑦 ≈ 𝑣)
53		isfi 8999	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ Fin ↔ ∃𝑣 ∈ ω 𝑦 ≈ 𝑣)
54	52, 53	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → 𝑦 ∈ Fin)
55		pm2.27 42	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ≈ 𝑣 → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒))
56	55	adantl 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒))
57		findcard2OLD.6	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃))
58	54, 56, 57	sylsyld 61	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜃))
59	51, 58	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → 𝜃))
60		vex 3466	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑦 ∈ V
61		snex 5429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑧} ∈ V
62	60, 61	unex 7746	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∪ {𝑧}) ∈ V
63		findcard2OLD.3	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))
64	62, 63	sbcie 3819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑 ↔ 𝜃)
65	59, 64	imbitrrdi 251	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑))
66	41, 47, 65	vtocl 3537	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
67		dfsbcq 3777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ([((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑 ↔ [𝑤 / 𝑥]𝜑))
68	67	imbi2d 339	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
69	66, 68	imbitrid 243	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
70	35, 39, 69	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
71	70	expd 414	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑤 → (𝑣 ∈ ω → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
72	71	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ω → (𝑧 ∈ 𝑤 → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
73	72	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧 ∈ 𝑤 → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
74	34, 73	mpdd 43	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧 ∈ 𝑤 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
75	74	exlimdv 1929	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∃𝑧 𝑧 ∈ 𝑤 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
76	32, 75	biimtrid 241	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
77	76	ex 411	. . . . . . . . . 10 ⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (𝑤 ≠ ∅ → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
78	31, 77	mpdd 43	. . . . . . . . 9 ⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
79	78	com23 86	. . . . . . . 8 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → (𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
80	79	alrimdv 1925	. . . . . . 7 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → ∀𝑤(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
81		nfv 1910	. . . . . . . 8 ⊢ Ⅎ𝑤(𝑥 ≈ suc 𝑣 → 𝜑)
82		nfv 1910	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑤 ≈ suc 𝑣
83		nfsbc1v 3795	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝜑
84	82, 83	nfim 1892	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)
85		breq1 5148	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑥 ≈ suc 𝑣 ↔ 𝑤 ≈ suc 𝑣))
86		sbceq1a 3786	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑))
87	85, 86	imbi12d 343	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ((𝑥 ≈ suc 𝑣 → 𝜑) ↔ (𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
88	81, 84, 87	cbvalv1 2332	. . . . . . 7 ⊢ (∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑) ↔ ∀𝑤(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑))
89	80, 88	imbitrrdi 251	. . . . . 6 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑)))
90	5, 8, 11, 17, 89	finds1 7904	. . . . 5 ⊢ (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑))
91	90	19.21bi 2178	. . . 4 ⊢ (𝑤 ∈ ω → (𝑥 ≈ 𝑤 → 𝜑))
92	91	rexlimiv 3138	. . 3 ⊢ (∃𝑤 ∈ ω 𝑥 ≈ 𝑤 → 𝜑)
93	2, 92	sylbi 216	. 2 ⊢ (𝑥 ∈ Fin → 𝜑)
94	1, 93	vtoclga 3557	1 ⊢ (𝐴 ∈ Fin → 𝜏)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394  ∀wal 1532   = wceq 1534  ∃wex 1774   ∈ wcel 2099   ≠ wne 2930  ∃wrex 3060  [wsbc 3775   ∖ cdif 3943   ∪ cun 3944   ⊆ wss 3946  ∅c0 4322  {csn 4623   class class class wbr 5145  suc csuc 6370  ωcom 7868   ≈ cen 8963  Fincfn 8966

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425  ax-un 7738

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-om 7869  df-1o 8488  df-en 8967  df-fin 8970

This theorem is referenced by: (None)