Theorem nncdiv3lem1 6276

Description: Lemma for nncdiv3 6278. Set up a helper for stratification. (Contributed by SF, 3-Mar-2015.)

Assertion

Ref	Expression
nncdiv3lem1	⊢ (⟨n, b⟩ ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd )) “ AddC )) ↔ b = ((n +c n) +c n))

Proof of Theorem nncdiv3lem1

Dummy variables m t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elrn2 4898	. 2 ⊢ (⟨n, b⟩ ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd )) “ AddC )) ↔ ∃m⟨m, ⟨n, b⟩⟩ ∈ ( Ins3 ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd )) “ AddC )))
2		elin 3220	. . . 4 ⊢ (⟨m, ⟨n, b⟩⟩ ∈ ( Ins3 ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd )) “ AddC )) ↔ (⟨m, ⟨n, b⟩⟩ ∈ Ins3 ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∧ ⟨m, ⟨n, b⟩⟩ ∈ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd )) “ AddC )))
3		vex 2863	. . . . . . 7 ⊢ b ∈ V
4	3	otelins3 5793	. . . . . 6 ⊢ (⟨m, ⟨n, b⟩⟩ ∈ Ins3 ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ↔ ⟨m, n⟩ ∈ ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ))
5		opelcnv 4894	. . . . . 6 ⊢ (⟨m, n⟩ ∈ ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ↔ ⟨n, m⟩ ∈ ((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ))
6		trtxp 5782	. . . . . . . . . 10 ⊢ (t(ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd )⟨n, m⟩ ↔ (tran (◡1st ⊗ (1st ∩ 2nd ))n ∧ t2nd m))
7		df-br 4641	. . . . . . . . . . . 12 ⊢ (tran (◡1st ⊗ (1st ∩ 2nd ))n ↔ ⟨t, n⟩ ∈ ran (◡1st ⊗ (1st ∩ 2nd )))
8		elrn2 4898	. . . . . . . . . . . 12 ⊢ (⟨t, n⟩ ∈ ran (◡1st ⊗ (1st ∩ 2nd )) ↔ ∃m⟨m, ⟨t, n⟩⟩ ∈ (◡1st ⊗ (1st ∩ 2nd )))
9		vex 2863	. . . . . . . . . . . . . . 15 ⊢ t ∈ V
10	9	proj1ex 4594	. . . . . . . . . . . . . 14 ⊢ Proj1 t ∈ V
11	10	eqvinc 2967	. . . . . . . . . . . . 13 ⊢ ( Proj1 t = ⟨n, n⟩ ↔ ∃m(m = Proj1 t ∧ m = ⟨n, n⟩))
12		opeq 4620	. . . . . . . . . . . . . . 15 ⊢ t = ⟨ Proj1 t, Proj2 t⟩
13	12	breq1i 4647	. . . . . . . . . . . . . 14 ⊢ (t1st ⟨n, n⟩ ↔ ⟨ Proj1 t, Proj2 t⟩1st ⟨n, n⟩)
14	9	proj2ex 4595	. . . . . . . . . . . . . . 15 ⊢ Proj2 t ∈ V
15	10, 14	opbr1st 5502	. . . . . . . . . . . . . 14 ⊢ (⟨ Proj1 t, Proj2 t⟩1st ⟨n, n⟩ ↔ Proj1 t = ⟨n, n⟩)
16	13, 15	bitri 240	. . . . . . . . . . . . 13 ⊢ (t1st ⟨n, n⟩ ↔ Proj1 t = ⟨n, n⟩)
17		oteltxp 5783	. . . . . . . . . . . . . . 15 ⊢ (⟨m, ⟨t, n⟩⟩ ∈ (◡1st ⊗ (1st ∩ 2nd )) ↔ (⟨m, t⟩ ∈ ◡1st ∧ ⟨m, n⟩ ∈ (1st ∩ 2nd )))
18		opelcnv 4894	. . . . . . . . . . . . . . . . 17 ⊢ (⟨m, t⟩ ∈ ◡1st ↔ ⟨t, m⟩ ∈ 1st )
19		df-br 4641	. . . . . . . . . . . . . . . . 17 ⊢ (t1st m ↔ ⟨t, m⟩ ∈ 1st )
20	12	breq1i 4647	. . . . . . . . . . . . . . . . . 18 ⊢ (t1st m ↔ ⟨ Proj1 t, Proj2 t⟩1st m)
21	10, 14	opbr1st 5502	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨ Proj1 t, Proj2 t⟩1st m ↔ Proj1 t = m)
22		eqcom 2355	. . . . . . . . . . . . . . . . . 18 ⊢ ( Proj1 t = m ↔ m = Proj1 t)
23	20, 21, 22	3bitri 262	. . . . . . . . . . . . . . . . 17 ⊢ (t1st m ↔ m = Proj1 t)
24	18, 19, 23	3bitr2i 264	. . . . . . . . . . . . . . . 16 ⊢ (⟨m, t⟩ ∈ ◡1st ↔ m = Proj1 t)
25		elin 3220	. . . . . . . . . . . . . . . . 17 ⊢ (⟨m, n⟩ ∈ (1st ∩ 2nd ) ↔ (⟨m, n⟩ ∈ 1st ∧ ⟨m, n⟩ ∈ 2nd ))
26		df-br 4641	. . . . . . . . . . . . . . . . . 18 ⊢ (m1st n ↔ ⟨m, n⟩ ∈ 1st )
27		df-br 4641	. . . . . . . . . . . . . . . . . 18 ⊢ (m2nd n ↔ ⟨m, n⟩ ∈ 2nd )
28	26, 27	anbi12i 678	. . . . . . . . . . . . . . . . 17 ⊢ ((m1st n ∧ m2nd n) ↔ (⟨m, n⟩ ∈ 1st ∧ ⟨m, n⟩ ∈ 2nd ))
29		vex 2863	. . . . . . . . . . . . . . . . . 18 ⊢ n ∈ V
30	29, 29	op1st2nd 5791	. . . . . . . . . . . . . . . . 17 ⊢ ((m1st n ∧ m2nd n) ↔ m = ⟨n, n⟩)
31	25, 28, 30	3bitr2i 264	. . . . . . . . . . . . . . . 16 ⊢ (⟨m, n⟩ ∈ (1st ∩ 2nd ) ↔ m = ⟨n, n⟩)
32	24, 31	anbi12i 678	. . . . . . . . . . . . . . 15 ⊢ ((⟨m, t⟩ ∈ ◡1st ∧ ⟨m, n⟩ ∈ (1st ∩ 2nd )) ↔ (m = Proj1 t ∧ m = ⟨n, n⟩))
33	17, 32	bitri 240	. . . . . . . . . . . . . 14 ⊢ (⟨m, ⟨t, n⟩⟩ ∈ (◡1st ⊗ (1st ∩ 2nd )) ↔ (m = Proj1 t ∧ m = ⟨n, n⟩))
34	33	exbii 1582	. . . . . . . . . . . . 13 ⊢ (∃m⟨m, ⟨t, n⟩⟩ ∈ (◡1st ⊗ (1st ∩ 2nd )) ↔ ∃m(m = Proj1 t ∧ m = ⟨n, n⟩))
35	11, 16, 34	3bitr4ri 269	. . . . . . . . . . . 12 ⊢ (∃m⟨m, ⟨t, n⟩⟩ ∈ (◡1st ⊗ (1st ∩ 2nd )) ↔ t1st ⟨n, n⟩)
36	7, 8, 35	3bitri 262	. . . . . . . . . . 11 ⊢ (tran (◡1st ⊗ (1st ∩ 2nd ))n ↔ t1st ⟨n, n⟩)
37	36	anbi1i 676	. . . . . . . . . 10 ⊢ ((tran (◡1st ⊗ (1st ∩ 2nd ))n ∧ t2nd m) ↔ (t1st ⟨n, n⟩ ∧ t2nd m))
38	29, 29	opex 4589	. . . . . . . . . . 11 ⊢ ⟨n, n⟩ ∈ V
39		vex 2863	. . . . . . . . . . 11 ⊢ m ∈ V
40	38, 39	op1st2nd 5791	. . . . . . . . . 10 ⊢ ((t1st ⟨n, n⟩ ∧ t2nd m) ↔ t = ⟨⟨n, n⟩, m⟩)
41	6, 37, 40	3bitri 262	. . . . . . . . 9 ⊢ (t(ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd )⟨n, m⟩ ↔ t = ⟨⟨n, n⟩, m⟩)
42	41	rexbii 2640	. . . . . . . 8 ⊢ (∃t ∈ AddC t(ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd )⟨n, m⟩ ↔ ∃t ∈ AddC t = ⟨⟨n, n⟩, m⟩)
43		elima 4755	. . . . . . . 8 ⊢ (⟨n, m⟩ ∈ ((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ↔ ∃t ∈ AddC t(ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd )⟨n, m⟩)
44		df-br 4641	. . . . . . . . 9 ⊢ (⟨n, n⟩ AddC m ↔ ⟨⟨n, n⟩, m⟩ ∈ AddC )
45		risset 2662	. . . . . . . . 9 ⊢ (⟨⟨n, n⟩, m⟩ ∈ AddC ↔ ∃t ∈ AddC t = ⟨⟨n, n⟩, m⟩)
46	44, 45	bitri 240	. . . . . . . 8 ⊢ (⟨n, n⟩ AddC m ↔ ∃t ∈ AddC t = ⟨⟨n, n⟩, m⟩)
47	42, 43, 46	3bitr4i 268	. . . . . . 7 ⊢ (⟨n, m⟩ ∈ ((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ↔ ⟨n, n⟩ AddC m)
48	29, 29	braddcfn 5827	. . . . . . 7 ⊢ (⟨n, n⟩ AddC m ↔ (n +c n) = m)
49		eqcom 2355	. . . . . . 7 ⊢ ((n +c n) = m ↔ m = (n +c n))
50	47, 48, 49	3bitri 262	. . . . . 6 ⊢ (⟨n, m⟩ ∈ ((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ↔ m = (n +c n))
51	4, 5, 50	3bitri 262	. . . . 5 ⊢ (⟨m, ⟨n, b⟩⟩ ∈ Ins3 ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ↔ m = (n +c n))
52		elima 4755	. . . . . . 7 ⊢ (⟨m, ⟨n, b⟩⟩ ∈ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd )) “ AddC ) ↔ ∃t ∈ AddC t((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))⟨m, ⟨n, b⟩⟩)
53		trtxp 5782	. . . . . . . . 9 ⊢ (t((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))⟨m, ⟨n, b⟩⟩ ↔ (t(1st ∘ 1st )m ∧ t((2nd ∘ 1st ) ⊗ 2nd )⟨n, b⟩))
54		trtxp 5782	. . . . . . . . . . 11 ⊢ (t((2nd ∘ 1st ) ⊗ 2nd )⟨n, b⟩ ↔ (t(2nd ∘ 1st )n ∧ t2nd b))
55	54	anbi2i 675	. . . . . . . . . 10 ⊢ ((t(1st ∘ 1st )m ∧ t((2nd ∘ 1st ) ⊗ 2nd )⟨n, b⟩) ↔ (t(1st ∘ 1st )m ∧ (t(2nd ∘ 1st )n ∧ t2nd b)))
56		anass 630	. . . . . . . . . 10 ⊢ (((t(1st ∘ 1st )m ∧ t(2nd ∘ 1st )n) ∧ t2nd b) ↔ (t(1st ∘ 1st )m ∧ (t(2nd ∘ 1st )n ∧ t2nd b)))
57	39, 29	op1st2nd 5791	. . . . . . . . . . . 12 ⊢ (( Proj1 t1st m ∧ Proj1 t2nd n) ↔ Proj1 t = ⟨m, n⟩)
58		brco 4884	. . . . . . . . . . . . . 14 ⊢ (t(1st ∘ 1st )m ↔ ∃n(t1st n ∧ n1st m))
59	12	breq1i 4647	. . . . . . . . . . . . . . . . 17 ⊢ (t1st n ↔ ⟨ Proj1 t, Proj2 t⟩1st n)
60	10, 14	opbr1st 5502	. . . . . . . . . . . . . . . . 17 ⊢ (⟨ Proj1 t, Proj2 t⟩1st n ↔ Proj1 t = n)
61		eqcom 2355	. . . . . . . . . . . . . . . . 17 ⊢ ( Proj1 t = n ↔ n = Proj1 t)
62	59, 60, 61	3bitri 262	. . . . . . . . . . . . . . . 16 ⊢ (t1st n ↔ n = Proj1 t)
63	62	anbi1i 676	. . . . . . . . . . . . . . 15 ⊢ ((t1st n ∧ n1st m) ↔ (n = Proj1 t ∧ n1st m))
64	63	exbii 1582	. . . . . . . . . . . . . 14 ⊢ (∃n(t1st n ∧ n1st m) ↔ ∃n(n = Proj1 t ∧ n1st m))
65		breq1 4643	. . . . . . . . . . . . . . 15 ⊢ (n = Proj1 t → (n1st m ↔ Proj1 t1st m))
66	10, 65	ceqsexv 2895	. . . . . . . . . . . . . 14 ⊢ (∃n(n = Proj1 t ∧ n1st m) ↔ Proj1 t1st m)
67	58, 64, 66	3bitri 262	. . . . . . . . . . . . 13 ⊢ (t(1st ∘ 1st )m ↔ Proj1 t1st m)
68		brco 4884	. . . . . . . . . . . . . 14 ⊢ (t(2nd ∘ 1st )n ↔ ∃m(t1st m ∧ m2nd n))
69	23	anbi1i 676	. . . . . . . . . . . . . . 15 ⊢ ((t1st m ∧ m2nd n) ↔ (m = Proj1 t ∧ m2nd n))
70	69	exbii 1582	. . . . . . . . . . . . . 14 ⊢ (∃m(t1st m ∧ m2nd n) ↔ ∃m(m = Proj1 t ∧ m2nd n))
71		breq1 4643	. . . . . . . . . . . . . . 15 ⊢ (m = Proj1 t → (m2nd n ↔ Proj1 t2nd n))
72	10, 71	ceqsexv 2895	. . . . . . . . . . . . . 14 ⊢ (∃m(m = Proj1 t ∧ m2nd n) ↔ Proj1 t2nd n)
73	68, 70, 72	3bitri 262	. . . . . . . . . . . . 13 ⊢ (t(2nd ∘ 1st )n ↔ Proj1 t2nd n)
74	67, 73	anbi12i 678	. . . . . . . . . . . 12 ⊢ ((t(1st ∘ 1st )m ∧ t(2nd ∘ 1st )n) ↔ ( Proj1 t1st m ∧ Proj1 t2nd n))
75	12	breq1i 4647	. . . . . . . . . . . . 13 ⊢ (t1st ⟨m, n⟩ ↔ ⟨ Proj1 t, Proj2 t⟩1st ⟨m, n⟩)
76	10, 14	opbr1st 5502	. . . . . . . . . . . . 13 ⊢ (⟨ Proj1 t, Proj2 t⟩1st ⟨m, n⟩ ↔ Proj1 t = ⟨m, n⟩)
77	75, 76	bitri 240	. . . . . . . . . . . 12 ⊢ (t1st ⟨m, n⟩ ↔ Proj1 t = ⟨m, n⟩)
78	57, 74, 77	3bitr4i 268	. . . . . . . . . . 11 ⊢ ((t(1st ∘ 1st )m ∧ t(2nd ∘ 1st )n) ↔ t1st ⟨m, n⟩)
79	78	anbi1i 676	. . . . . . . . . 10 ⊢ (((t(1st ∘ 1st )m ∧ t(2nd ∘ 1st )n) ∧ t2nd b) ↔ (t1st ⟨m, n⟩ ∧ t2nd b))
80	55, 56, 79	3bitr2i 264	. . . . . . . . 9 ⊢ ((t(1st ∘ 1st )m ∧ t((2nd ∘ 1st ) ⊗ 2nd )⟨n, b⟩) ↔ (t1st ⟨m, n⟩ ∧ t2nd b))
81	39, 29	opex 4589	. . . . . . . . . 10 ⊢ ⟨m, n⟩ ∈ V
82	81, 3	op1st2nd 5791	. . . . . . . . 9 ⊢ ((t1st ⟨m, n⟩ ∧ t2nd b) ↔ t = ⟨⟨m, n⟩, b⟩)
83	53, 80, 82	3bitri 262	. . . . . . . 8 ⊢ (t((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))⟨m, ⟨n, b⟩⟩ ↔ t = ⟨⟨m, n⟩, b⟩)
84	83	rexbii 2640	. . . . . . 7 ⊢ (∃t ∈ AddC t((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))⟨m, ⟨n, b⟩⟩ ↔ ∃t ∈ AddC t = ⟨⟨m, n⟩, b⟩)
85	52, 84	bitri 240	. . . . . 6 ⊢ (⟨m, ⟨n, b⟩⟩ ∈ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd )) “ AddC ) ↔ ∃t ∈ AddC t = ⟨⟨m, n⟩, b⟩)
86		df-br 4641	. . . . . . 7 ⊢ (⟨m, n⟩ AddC b ↔ ⟨⟨m, n⟩, b⟩ ∈ AddC )
87		risset 2662	. . . . . . 7 ⊢ (⟨⟨m, n⟩, b⟩ ∈ AddC ↔ ∃t ∈ AddC t = ⟨⟨m, n⟩, b⟩)
88	86, 87	bitr2i 241	. . . . . 6 ⊢ (∃t ∈ AddC t = ⟨⟨m, n⟩, b⟩ ↔ ⟨m, n⟩ AddC b)
89	39, 29	braddcfn 5827	. . . . . . 7 ⊢ (⟨m, n⟩ AddC b ↔ (m +c n) = b)
90		eqcom 2355	. . . . . . 7 ⊢ ((m +c n) = b ↔ b = (m +c n))
91	89, 90	bitri 240	. . . . . 6 ⊢ (⟨m, n⟩ AddC b ↔ b = (m +c n))
92	85, 88, 91	3bitri 262	. . . . 5 ⊢ (⟨m, ⟨n, b⟩⟩ ∈ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd )) “ AddC ) ↔ b = (m +c n))
93	51, 92	anbi12i 678	. . . 4 ⊢ ((⟨m, ⟨n, b⟩⟩ ∈ Ins3 ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∧ ⟨m, ⟨n, b⟩⟩ ∈ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd )) “ AddC )) ↔ (m = (n +c n) ∧ b = (m +c n)))
94	2, 93	bitri 240	. . 3 ⊢ (⟨m, ⟨n, b⟩⟩ ∈ ( Ins3 ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd )) “ AddC )) ↔ (m = (n +c n) ∧ b = (m +c n)))
95	94	exbii 1582	. 2 ⊢ (∃m⟨m, ⟨n, b⟩⟩ ∈ ( Ins3 ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd )) “ AddC )) ↔ ∃m(m = (n +c n) ∧ b = (m +c n)))
96	29, 29	addcex 4395	. . 3 ⊢ (n +c n) ∈ V
97		addceq1 4384	. . . 4 ⊢ (m = (n +c n) → (m +c n) = ((n +c n) +c n))
98	97	eqeq2d 2364	. . 3 ⊢ (m = (n +c n) → (b = (m +c n) ↔ b = ((n +c n) +c n)))
99	96, 98	ceqsexv 2895	. 2 ⊢ (∃m(m = (n +c n) ∧ b = (m +c n)) ↔ b = ((n +c n) +c n))
100	1, 95, 99	3bitri 262	1 ⊢ (⟨n, b⟩ ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd )) “ AddC )) ↔ b = ((n +c n) +c n))

This proof depends on syntax axioms:   ↔ wb 176   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∃wrex 2616   ∩ cin 3209   +_c cplc 4376  ⟨cop 4562   Proj1 cproj1 4564   Proj2 cproj2 4565   class class class wbr 4640  1^st c1st 4718   ∘ ccom 4722   “ cima 4723  ^◡ccnv 4772  ran crn 4774  2^nd c2nd 4784   ⊗ ctxp 5736   AddC caddcfn 5746   Ins3 cins3 5752

This proof depends on 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 proof 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-co 4727  df-ima 4728  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-fo 4794  df-fv 4796  df-2nd 4798  df-ov 5527  df-oprab 5529  df-mpt 5653  df-mpt2 5655  df-txp 5737  df-addcfn 5747  df-ins3 5753

This theorem is used by:  nncdiv3lem2  6277  nnc3n3p1  6279