Theorem nmembers1lem3 6271

Description: Lemma for nmembers1 6272. If the interval from one to a natural is in a given natural, extending it by one puts it in the next natural. (Contributed by Scott Fenton, 3-Aug-2019.)

Assertion

Ref	Expression
nmembers1lem3	⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∈ B → {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} ∈ (B +c 1c)))

Distinct variable groups:   A,m   B,m

Proof of Theorem nmembers1lem3

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnltp1c 6263	. . . . . . . . . . . 12 ⊢ (A ∈ Nn → A <c (A +c 1c))
2		nnnc 6147	. . . . . . . . . . . . 13 ⊢ (A ∈ Nn → A ∈ NC )
3		peano2 4404	. . . . . . . . . . . . . 14 ⊢ (A ∈ Nn → (A +c 1c) ∈ Nn )
4		nnnc 6147	. . . . . . . . . . . . . 14 ⊢ ((A +c 1c) ∈ Nn → (A +c 1c) ∈ NC )
5	3, 4	syl 15	. . . . . . . . . . . . 13 ⊢ (A ∈ Nn → (A +c 1c) ∈ NC )
6		ltlenlec 6208	. . . . . . . . . . . . 13 ⊢ ((A ∈ NC ∧ (A +c 1c) ∈ NC ) → (A <c (A +c 1c) ↔ (A ≤c (A +c 1c) ∧ ¬ (A +c 1c) ≤c A)))
7	2, 5, 6	syl2anc 642	. . . . . . . . . . . 12 ⊢ (A ∈ Nn → (A <c (A +c 1c) ↔ (A ≤c (A +c 1c) ∧ ¬ (A +c 1c) ≤c A)))
8	1, 7	mpbid 201	. . . . . . . . . . 11 ⊢ (A ∈ Nn → (A ≤c (A +c 1c) ∧ ¬ (A +c 1c) ≤c A))
9	8	simprd 449	. . . . . . . . . 10 ⊢ (A ∈ Nn → ¬ (A +c 1c) ≤c A)
10	9	adantr 451	. . . . . . . . 9 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬ (A +c 1c) ≤c A)
11	10	intnand 882	. . . . . . . 8 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬ (1c ≤c (A +c 1c) ∧ (A +c 1c) ≤c A))
12	11	a1d 22	. . . . . . 7 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ((A +c 1c) ∈ Nn → ¬ (1c ≤c (A +c 1c) ∧ (A +c 1c) ≤c A)))
13		breq2 4644	. . . . . . . . . . 11 ⊢ (m = (A +c 1c) → (1c ≤c m ↔ 1c ≤c (A +c 1c)))
14		breq1 4643	. . . . . . . . . . 11 ⊢ (m = (A +c 1c) → (m ≤c A ↔ (A +c 1c) ≤c A))
15	13, 14	anbi12d 691	. . . . . . . . . 10 ⊢ (m = (A +c 1c) → ((1c ≤c m ∧ m ≤c A) ↔ (1c ≤c (A +c 1c) ∧ (A +c 1c) ≤c A)))
16	15	elrab 2995	. . . . . . . . 9 ⊢ ((A +c 1c) ∈ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ↔ ((A +c 1c) ∈ Nn ∧ (1c ≤c (A +c 1c) ∧ (A +c 1c) ≤c A)))
17	16	notbii 287	. . . . . . . 8 ⊢ (¬ (A +c 1c) ∈ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ↔ ¬ ((A +c 1c) ∈ Nn ∧ (1c ≤c (A +c 1c) ∧ (A +c 1c) ≤c A)))
18		imnan 411	. . . . . . . 8 ⊢ (((A +c 1c) ∈ Nn → ¬ (1c ≤c (A +c 1c) ∧ (A +c 1c) ≤c A)) ↔ ¬ ((A +c 1c) ∈ Nn ∧ (1c ≤c (A +c 1c) ∧ (A +c 1c) ≤c A)))
19	17, 18	bitr4i 243	. . . . . . 7 ⊢ (¬ (A +c 1c) ∈ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ↔ ((A +c 1c) ∈ Nn → ¬ (1c ≤c (A +c 1c) ∧ (A +c 1c) ≤c A)))
20	12, 19	sylibr 203	. . . . . 6 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬ (A +c 1c) ∈ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)})
21	3	adantr 451	. . . . . . 7 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → (A +c 1c) ∈ Nn )
22		elcomplg 3219	. . . . . . 7 ⊢ ((A +c 1c) ∈ Nn → ((A +c 1c) ∈ ∼ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ↔ ¬ (A +c 1c) ∈ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)}))
23	21, 22	syl 15	. . . . . 6 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ((A +c 1c) ∈ ∼ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ↔ ¬ (A +c 1c) ∈ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)}))
24	20, 23	mpbird 223	. . . . 5 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → (A +c 1c) ∈ ∼ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)})
25		nnnc 6147	. . . . . . . . . . . . . 14 ⊢ (x ∈ Nn → x ∈ NC )
26		ncslesuc 6268	. . . . . . . . . . . . . 14 ⊢ ((x ∈ NC ∧ A ∈ NC ) → (x ≤c (A +c 1c) ↔ (x ≤c A ∨ x = (A +c 1c))))
27	25, 2, 26	syl2an 463	. . . . . . . . . . . . 13 ⊢ ((x ∈ Nn ∧ A ∈ Nn ) → (x ≤c (A +c 1c) ↔ (x ≤c A ∨ x = (A +c 1c))))
28	27	expcom 424	. . . . . . . . . . . 12 ⊢ (A ∈ Nn → (x ∈ Nn → (x ≤c (A +c 1c) ↔ (x ≤c A ∨ x = (A +c 1c)))))
29	28	adantrd 454	. . . . . . . . . . 11 ⊢ (A ∈ Nn → ((x ∈ Nn ∧ 1c ≤c x) → (x ≤c (A +c 1c) ↔ (x ≤c A ∨ x = (A +c 1c)))))
30	29	adantr 451	. . . . . . . . . 10 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ((x ∈ Nn ∧ 1c ≤c x) → (x ≤c (A +c 1c) ↔ (x ≤c A ∨ x = (A +c 1c)))))
31	30	pm5.32d 620	. . . . . . . . 9 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → (((x ∈ Nn ∧ 1c ≤c x) ∧ x ≤c (A +c 1c)) ↔ ((x ∈ Nn ∧ 1c ≤c x) ∧ (x ≤c A ∨ x = (A +c 1c)))))
32		anass 630	. . . . . . . . 9 ⊢ (((x ∈ Nn ∧ 1c ≤c x) ∧ x ≤c (A +c 1c)) ↔ (x ∈ Nn ∧ (1c ≤c x ∧ x ≤c (A +c 1c))))
33		andi 837	. . . . . . . . . 10 ⊢ (((x ∈ Nn ∧ 1c ≤c x) ∧ (x ≤c A ∨ x = (A +c 1c))) ↔ (((x ∈ Nn ∧ 1c ≤c x) ∧ x ≤c A) ∨ ((x ∈ Nn ∧ 1c ≤c x) ∧ x = (A +c 1c))))
34		anass 630	. . . . . . . . . . 11 ⊢ (((x ∈ Nn ∧ 1c ≤c x) ∧ x ≤c A) ↔ (x ∈ Nn ∧ (1c ≤c x ∧ x ≤c A)))
35	34	orbi1i 506	. . . . . . . . . 10 ⊢ ((((x ∈ Nn ∧ 1c ≤c x) ∧ x ≤c A) ∨ ((x ∈ Nn ∧ 1c ≤c x) ∧ x = (A +c 1c))) ↔ ((x ∈ Nn ∧ (1c ≤c x ∧ x ≤c A)) ∨ ((x ∈ Nn ∧ 1c ≤c x) ∧ x = (A +c 1c))))
36	33, 35	bitri 240	. . . . . . . . 9 ⊢ (((x ∈ Nn ∧ 1c ≤c x) ∧ (x ≤c A ∨ x = (A +c 1c))) ↔ ((x ∈ Nn ∧ (1c ≤c x ∧ x ≤c A)) ∨ ((x ∈ Nn ∧ 1c ≤c x) ∧ x = (A +c 1c))))
37	31, 32, 36	3bitr3g 278	. . . . . . . 8 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ((x ∈ Nn ∧ (1c ≤c x ∧ x ≤c (A +c 1c))) ↔ ((x ∈ Nn ∧ (1c ≤c x ∧ x ≤c A)) ∨ ((x ∈ Nn ∧ 1c ≤c x) ∧ x = (A +c 1c)))))
38		1cnc 6140	. . . . . . . . . . . . . . . 16 ⊢ 1c ∈ NC
39		addlecncs 6210	. . . . . . . . . . . . . . . 16 ⊢ ((1c ∈ NC ∧ A ∈ NC ) → 1c ≤c (1c +c A))
40	38, 2, 39	sylancr 644	. . . . . . . . . . . . . . 15 ⊢ (A ∈ Nn → 1c ≤c (1c +c A))
41		addccom 4407	. . . . . . . . . . . . . . 15 ⊢ (A +c 1c) = (1c +c A)
42	40, 41	syl6breqr 4680	. . . . . . . . . . . . . 14 ⊢ (A ∈ Nn → 1c ≤c (A +c 1c))
43	3, 42	jca 518	. . . . . . . . . . . . 13 ⊢ (A ∈ Nn → ((A +c 1c) ∈ Nn ∧ 1c ≤c (A +c 1c)))
44		eleq1 2413	. . . . . . . . . . . . . 14 ⊢ (x = (A +c 1c) → (x ∈ Nn ↔ (A +c 1c) ∈ Nn ))
45		breq2 4644	. . . . . . . . . . . . . 14 ⊢ (x = (A +c 1c) → (1c ≤c x ↔ 1c ≤c (A +c 1c)))
46	44, 45	anbi12d 691	. . . . . . . . . . . . 13 ⊢ (x = (A +c 1c) → ((x ∈ Nn ∧ 1c ≤c x) ↔ ((A +c 1c) ∈ Nn ∧ 1c ≤c (A +c 1c))))
47	43, 46	syl5ibrcom 213	. . . . . . . . . . . 12 ⊢ (A ∈ Nn → (x = (A +c 1c) → (x ∈ Nn ∧ 1c ≤c x)))
48	47	adantr 451	. . . . . . . . . . 11 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → (x = (A +c 1c) → (x ∈ Nn ∧ 1c ≤c x)))
49	48	pm4.71rd 616	. . . . . . . . . 10 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → (x = (A +c 1c) ↔ ((x ∈ Nn ∧ 1c ≤c x) ∧ x = (A +c 1c))))
50	49	bicomd 192	. . . . . . . . 9 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → (((x ∈ Nn ∧ 1c ≤c x) ∧ x = (A +c 1c)) ↔ x = (A +c 1c)))
51	50	orbi2d 682	. . . . . . . 8 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → (((x ∈ Nn ∧ (1c ≤c x ∧ x ≤c A)) ∨ ((x ∈ Nn ∧ 1c ≤c x) ∧ x = (A +c 1c))) ↔ ((x ∈ Nn ∧ (1c ≤c x ∧ x ≤c A)) ∨ x = (A +c 1c))))
52	37, 51	bitrd 244	. . . . . . 7 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ((x ∈ Nn ∧ (1c ≤c x ∧ x ≤c (A +c 1c))) ↔ ((x ∈ Nn ∧ (1c ≤c x ∧ x ≤c A)) ∨ x = (A +c 1c))))
53		breq2 4644	. . . . . . . . 9 ⊢ (m = x → (1c ≤c m ↔ 1c ≤c x))
54		breq1 4643	. . . . . . . . 9 ⊢ (m = x → (m ≤c (A +c 1c) ↔ x ≤c (A +c 1c)))
55	53, 54	anbi12d 691	. . . . . . . 8 ⊢ (m = x → ((1c ≤c m ∧ m ≤c (A +c 1c)) ↔ (1c ≤c x ∧ x ≤c (A +c 1c))))
56	55	elrab 2995	. . . . . . 7 ⊢ (x ∈ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} ↔ (x ∈ Nn ∧ (1c ≤c x ∧ x ≤c (A +c 1c))))
57		elun 3221	. . . . . . . 8 ⊢ (x ∈ ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {(A +c 1c)}) ↔ (x ∈ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∨ x ∈ {(A +c 1c)}))
58		breq1 4643	. . . . . . . . . . 11 ⊢ (m = x → (m ≤c A ↔ x ≤c A))
59	53, 58	anbi12d 691	. . . . . . . . . 10 ⊢ (m = x → ((1c ≤c m ∧ m ≤c A) ↔ (1c ≤c x ∧ x ≤c A)))
60	59	elrab 2995	. . . . . . . . 9 ⊢ (x ∈ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ↔ (x ∈ Nn ∧ (1c ≤c x ∧ x ≤c A)))
61		elsn 3749	. . . . . . . . 9 ⊢ (x ∈ {(A +c 1c)} ↔ x = (A +c 1c))
62	60, 61	orbi12i 507	. . . . . . . 8 ⊢ ((x ∈ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∨ x ∈ {(A +c 1c)}) ↔ ((x ∈ Nn ∧ (1c ≤c x ∧ x ≤c A)) ∨ x = (A +c 1c)))
63	57, 62	bitri 240	. . . . . . 7 ⊢ (x ∈ ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {(A +c 1c)}) ↔ ((x ∈ Nn ∧ (1c ≤c x ∧ x ≤c A)) ∨ x = (A +c 1c)))
64	52, 56, 63	3bitr4g 279	. . . . . 6 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → (x ∈ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} ↔ x ∈ ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {(A +c 1c)})))
65	64	eqrdv 2351	. . . . 5 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {(A +c 1c)}))
66		sneq 3745	. . . . . . . 8 ⊢ (y = (A +c 1c) → {y} = {(A +c 1c)})
67	66	uneq2d 3419	. . . . . . 7 ⊢ (y = (A +c 1c) → ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {y}) = ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {(A +c 1c)}))
68	67	eqeq2d 2364	. . . . . 6 ⊢ (y = (A +c 1c) → ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {y}) ↔ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {(A +c 1c)})))
69	68	rspcev 2956	. . . . 5 ⊢ (((A +c 1c) ∈ ∼ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∧ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {(A +c 1c)})) → ∃y ∈ ∼ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {y}))
70	24, 65, 69	syl2anc 642	. . . 4 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ∃y ∈ ∼ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {y}))
71		compleq 3244	. . . . . 6 ⊢ (x = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} → ∼ x = ∼ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)})
72		uneq1 3412	. . . . . . 7 ⊢ (x = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} → (x ∪ {y}) = ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {y}))
73	72	eqeq2d 2364	. . . . . 6 ⊢ (x = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} → ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = (x ∪ {y}) ↔ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {y})))
74	71, 73	rexeqbidv 2821	. . . . 5 ⊢ (x = {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} → (∃y ∈ ∼ x{m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = (x ∪ {y}) ↔ ∃y ∈ ∼ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {y})))
75	74	rspcev 2956	. . . 4 ⊢ (({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∈ B ∧ ∃y ∈ ∼ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∪ {y})) → ∃x ∈ B ∃y ∈ ∼ x{m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = (x ∪ {y}))
76	70, 75	sylan2 460	. . 3 ⊢ (({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∈ B ∧ (A ∈ Nn ∧ B ∈ Nn )) → ∃x ∈ B ∃y ∈ ∼ x{m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = (x ∪ {y}))
77		elsuc 4414	. . 3 ⊢ ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} ∈ (B +c 1c) ↔ ∃x ∈ B ∃y ∈ ∼ x{m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} = (x ∪ {y}))
78	76, 77	sylibr 203	. 2 ⊢ (({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∈ B ∧ (A ∈ Nn ∧ B ∈ Nn )) → {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} ∈ (B +c 1c))
79	78	expcom 424	1 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∈ B → {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} ∈ (B +c 1c)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   = wceq 1642   ∈ wcel 1710  ∃wrex 2616  {crab 2619   ∼ ccompl 3206   ∪ cun 3208  {csn 3738  1_cc1c 4135   Nn cnnc 4374   +_c cplc 4376   class class class wbr 4640   NC cncs 6089   ≤_c clec 6090   <_c cltc 6091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-rab 2624  df-v 2862  df-sbc 3048  df-csb 3138  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-pss 3262  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-iun 3972  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-0c 4378  df-addc 4379  df-nnc 4380  df-fin 4381  df-lefin 4441  df-ltfin 4442  df-ncfin 4443  df-tfin 4444  df-evenfin 4445  df-oddfin 4446  df-sfin 4447  df-spfin 4448  df-phi 4566  df-op 4567  df-proj1 4568  df-proj2 4569  df-opab 4624  df-br 4641  df-1st 4724  df-swap 4725  df-sset 4726  df-co 4727  df-ima 4728  df-si 4729  df-id 4768  df-xp 4785  df-cnv 4786  df-rn 4787  df-dm 4788  df-res 4789  df-fun 4790  df-fn 4791  df-f 4792  df-f1 4793  df-fo 4794  df-f1o 4795  df-fv 4796  df-2nd 4798  df-ov 5527  df-oprab 5529  df-mpt 5653  df-mpt2 5655  df-txp 5737  df-fix 5741  df-cup 5743  df-disj 5745  df-addcfn 5747  df-ins2 5751  df-ins3 5753  df-image 5755  df-ins4 5757  df-si3 5759  df-funs 5761  df-fns 5763  df-clos1 5874  df-trans 5900  df-sym 5909  df-er 5910  df-ec 5948  df-qs 5952  df-en 6030  df-ncs 6099  df-lec 6100  df-ltc 6101  df-nc 6102

This theorem is referenced by:  nmembers1  6272