Theorem findcard2OLD 8986

Description: Obsolete version of findcard2 8909 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 8719	. . 3 ⊢ (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥 ≈ 𝑤)
3		breq2 5074	. . . . . . . 8 ⊢ (𝑤 = ∅ → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ ∅))
4	3	imbi1d 341	. . . . . . 7 ⊢ (𝑤 = ∅ → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ ∅ → 𝜑)))
5	4	albidv 1924	. . . . . 6 ⊢ (𝑤 = ∅ → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑)))
6		breq2 5074	. . . . . . . 8 ⊢ (𝑤 = 𝑣 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ 𝑣))
7	6	imbi1d 341	. . . . . . 7 ⊢ (𝑤 = 𝑣 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ 𝑣 → 𝜑)))
8	7	albidv 1924	. . . . . 6 ⊢ (𝑤 = 𝑣 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ 𝑣 → 𝜑)))
9		breq2 5074	. . . . . . . 8 ⊢ (𝑤 = suc 𝑣 → (𝑥 ≈ 𝑤 ↔ 𝑥 ≈ suc 𝑣))
10	9	imbi1d 341	. . . . . . 7 ⊢ (𝑤 = suc 𝑣 → ((𝑥 ≈ 𝑤 → 𝜑) ↔ (𝑥 ≈ suc 𝑣 → 𝜑)))
11	10	albidv 1924	. . . . . 6 ⊢ (𝑤 = suc 𝑣 → (∀𝑥(𝑥 ≈ 𝑤 → 𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑)))
12		en0 8758	. . . . . . . 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 1799	. . . . . 6 ⊢ ∀𝑥(𝑥 ≈ ∅ → 𝜑)
18		nsuceq0 6331	. . . . . . . . . . . 12 ⊢ suc 𝑣 ≠ ∅
19		breq1 5073	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ∅ → (𝑤 ≈ suc 𝑣 ↔ ∅ ≈ suc 𝑣))
20	19	anbi2d 628	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) ↔ (𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣)))
21		peano1 7710	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ ω
22		peano2 7711	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ ω → suc 𝑣 ∈ ω)
23		nneneq 8896	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ ω ∧ suc 𝑣 ∈ ω) → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
24	21, 22, 23	sylancr 586	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ ω → (∅ ≈ suc 𝑣 ↔ ∅ = suc 𝑣))
25	24	biimpa 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → ∅ = suc 𝑣)
26	25	eqcomd 2744	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ ω ∧ ∅ ≈ suc 𝑣) → suc 𝑣 = ∅)
27	20, 26	syl6bi 252	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ∅ → ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → suc 𝑣 = ∅))
28	27	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 = ∅ → suc 𝑣 = ∅))
29	28	necon3d 2963	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (suc 𝑣 ≠ ∅ → 𝑤 ≠ ∅))
30	18, 29	mpi 20	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → 𝑤 ≠ ∅)
31	30	ex 412	. . . . . . . . . 10 ⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → 𝑤 ≠ ∅))
32		n0 4277	. . . . . . . . . . . 12 ⊢ (𝑤 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝑤)
33		dif1en 8907	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣 ∧ 𝑧 ∈ 𝑤) → (𝑤 ∖ {𝑧}) ≈ 𝑣)
34	33	3expia 1119	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧 ∈ 𝑤 → (𝑤 ∖ {𝑧}) ≈ 𝑣))
35		snssi 4738	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑤 → {𝑧} ⊆ 𝑤)
36		uncom 4083	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = ({𝑧} ∪ (𝑤 ∖ {𝑧}))
37		undif 4412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑧} ⊆ 𝑤 ↔ ({𝑧} ∪ (𝑤 ∖ {𝑧})) = 𝑤)
38	37	biimpi 215	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑧} ⊆ 𝑤 → ({𝑧} ∪ (𝑤 ∖ {𝑧})) = 𝑤)
39	36, 38	eqtrid 2790	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑧} ⊆ 𝑤 → ((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤)
40		vex 3426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑤 ∈ V
41	40	difexi 5247	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∖ {𝑧}) ∈ V
42		breq1 5073	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ≈ 𝑣 ↔ (𝑤 ∖ {𝑧}) ≈ 𝑣))
43	42	anbi2d 628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) ↔ (𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣)))
44		uneq1 4086	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (𝑦 ∪ {𝑧}) = ((𝑤 ∖ {𝑧}) ∪ {𝑧}))
45	44	sbceq1d 3716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑 ↔ [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
46	45	imbi2d 340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → ((∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑)))
47	43, 46	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑤 ∖ {𝑧}) → (((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑)) ↔ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))))
48		breq1 5073	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑣 ↔ 𝑦 ≈ 𝑣))
49		findcard2OLD.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
50	48, 49	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑣 → 𝜑) ↔ (𝑦 ≈ 𝑣 → 𝜒)))
51	50	spvv 2001	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → (𝑦 ≈ 𝑣 → 𝜒))
52		rspe 3232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ∃𝑣 ∈ ω 𝑦 ≈ 𝑣)
53		isfi 8719	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ Fin ↔ ∃𝑣 ∈ ω 𝑦 ≈ 𝑣)
54	52, 53	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → 𝑦 ∈ Fin)
55		pm2.27 42	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ≈ 𝑣 → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒))
56	55	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜒))
57		findcard2OLD.6	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃))
58	54, 56, 57	sylsyld 61	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → ((𝑦 ≈ 𝑣 → 𝜒) → 𝜃))
59	51, 58	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → 𝜃))
60		vex 3426	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑦 ∈ V
61		snex 5349	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑧} ∈ V
62	60, 61	unex 7574	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∪ {𝑧}) ∈ V
63		findcard2OLD.3	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))
64	62, 63	sbcie 3754	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ([(𝑦 ∪ {𝑧}) / 𝑥]𝜑 ↔ 𝜃)
65	59, 64	syl6ibr 251	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 ∈ ω ∧ 𝑦 ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [(𝑦 ∪ {𝑧}) / 𝑥]𝜑))
66	41, 47, 65	vtocl 3488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑))
67		dfsbcq 3713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ([((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑 ↔ [𝑤 / 𝑥]𝜑))
68	67	imbi2d 340	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [((𝑤 ∖ {𝑧}) ∪ {𝑧}) / 𝑥]𝜑) ↔ (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
69	66, 68	syl5ib 243	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∖ {𝑧}) ∪ {𝑧}) = 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
70	35, 39, 69	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑤 → ((𝑣 ∈ ω ∧ (𝑤 ∖ {𝑧}) ≈ 𝑣) → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
71	70	expd 415	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑤 → (𝑣 ∈ ω → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
72	71	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ω → (𝑧 ∈ 𝑤 → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
73	72	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧 ∈ 𝑤 → ((𝑤 ∖ {𝑧}) ≈ 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
74	34, 73	mpdd 43	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑧 ∈ 𝑤 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
75	74	exlimdv 1937	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (∃𝑧 𝑧 ∈ 𝑤 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
76	32, 75	syl5bi 241	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ω ∧ 𝑤 ≈ suc 𝑣) → (𝑤 ≠ ∅ → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
77	76	ex 412	. . . . . . . . . 10 ⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (𝑤 ≠ ∅ → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑))))
78	31, 77	mpdd 43	. . . . . . . . 9 ⊢ (𝑣 ∈ ω → (𝑤 ≈ suc 𝑣 → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → [𝑤 / 𝑥]𝜑)))
79	78	com23 86	. . . . . . . 8 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → (𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
80	79	alrimdv 1933	. . . . . . 7 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → ∀𝑤(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
81		nfv 1918	. . . . . . . 8 ⊢ Ⅎ𝑤(𝑥 ≈ suc 𝑣 → 𝜑)
82		nfv 1918	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑤 ≈ suc 𝑣
83		nfsbc1v 3731	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝜑
84	82, 83	nfim 1900	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)
85		breq1 5073	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑥 ≈ suc 𝑣 ↔ 𝑤 ≈ suc 𝑣))
86		sbceq1a 3722	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑))
87	85, 86	imbi12d 344	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ((𝑥 ≈ suc 𝑣 → 𝜑) ↔ (𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑)))
88	81, 84, 87	cbvalv1 2340	. . . . . . 7 ⊢ (∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑) ↔ ∀𝑤(𝑤 ≈ suc 𝑣 → [𝑤 / 𝑥]𝜑))
89	80, 88	syl6ibr 251	. . . . . 6 ⊢ (𝑣 ∈ ω → (∀𝑥(𝑥 ≈ 𝑣 → 𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣 → 𝜑)))
90	5, 8, 11, 17, 89	finds1 7722	. . . . 5 ⊢ (𝑤 ∈ ω → ∀𝑥(𝑥 ≈ 𝑤 → 𝜑))
91	90	19.21bi 2184	. . . 4 ⊢ (𝑤 ∈ ω → (𝑥 ≈ 𝑤 → 𝜑))
92	91	rexlimiv 3208	. . 3 ⊢ (∃𝑤 ∈ ω 𝑥 ≈ 𝑤 → 𝜑)
93	2, 92	sylbi 216	. 2 ⊢ (𝑥 ∈ Fin → 𝜑)
94	1, 93	vtoclga 3503	1 ⊢ (𝐴 ∈ Fin → 𝜏)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∃wrex 3064  [wsbc 3711   ∖ cdif 3880   ∪ cun 3881   ⊆ wss 3883  ∅c0 4253  {csn 4558   class class class wbr 5070  suc csuc 6253  ωcom 7687   ≈ cen 8688  Fincfn 8691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-om 7688  df-er 8456  df-en 8692  df-fin 8695

This theorem is referenced by: (None)